[Agda] Coding Conventions

[Vag Vagoff]

> Some people tend to follow the convention that types are capitalised,
> whereas constructors are not (assuming that the names start with
> suitable characters).

But what about uncapitalisable constructors? I propose MIDDLE DOT 
(U+00B7) for this purpose:

infix 6 _↔_
data _↔_ (P Q : Set) : Set where
     ·↔· : (P → Q) → (Q → P) → P ↔ Q

infix 11 _↭_
data _↭_ {a : A} (P Q : Term a) : Set where
     ·↝· : P ↝ Q → P ↭ Q
     ·↜· : Q ↝ P → P ↭ Q
     ·↭·↭· : ∀ {T} → P ↭ T → T ↭ Q → P ↭ Q

infix 11 _↭°_
data _↭°_ {a : A} : Term a → Term a → Set where
     ·↭· : ∀ {P P'} → P ↭ P' → P ↭° P'
     · : ∀ {P} → P ↭° P