Agda users rely heavily on unicode. It looks like they have editor support for it in the form of backslash sequences that turn into unicode. They write stuff l

Agda users rely heavily on unicode. It looks like they have editor support for it in the form of backslash sequences that turn into unicode. They write stuff like: Tyᴹ : (A : Ty) → {X₀ X₁ : Set} → (X₀ → X₁) → Tyᴬ A X₀ → Tyᴬ A X₁ → Set Tyᴹ ι Xᴹ α₀ α₁ = Xᴹ α₀ ≡ α₁ Tyᴹ (ι⇒ A) Xᴹ α₀ α₁ = ∀ x → Tyᴹ A Xᴹ (α₀ x ) (α₁ (Xᴹ x)) I kind of get the "looks like math" thing, but I find the poor typography distracting. (Sample taken from https://github.com/AndrasKovacs/thesis/blob/main/agda/SimpleSig.agda https://github.com/AndrasKovacs/thesis/blob/main/agda/Simple... - learning the language is still on my todo list.)