enforce naming policy regarding numerical superscripts

NAMING.md

@@ -21,9 +21,12 @@ For naming conventions specific to the Algebra subfolder, see
   (for example `is-prop`).
 
 * Use abbreviations to avoid very long names, e.g.
+  - `id-l`/`id-r` = identity on the left/right
   - `comm` = commutative
   - `assoc` = associative
-  - `dist-r`/`dist-l` = distribute right/left
+  - `idem` = idempotent
+  - `absorp` = absorptive
+  - `dist-l`/`dist-r` = distribute left/right
   - `comp` = composition
   - `Cat` = category
   - `hom` = homomorphism
@@ -36,10 +39,15 @@ For naming conventions specific to the Algebra subfolder, see
 * Avoid referring to variable names in the names of definitions.
   For example, prefer `+-comm` to something like `m+n≡n+m`.
 
-* Use `Equiv` or `≃` to refer to equivalences of types or structures.
+* Numerical superscripts must be used only for arity specification.
+
+  Numerical subscripts should be preferred to indicate hlevel, but
+  can be used for other purposes if it improves readability.
+
+* Use `equiv` or `≃` to refer to equivalences of types or structures.
   Operators can use subscript `ₑ`.
 
-* Use `Iso` or `≅` to refer to isomorphisms of types or structures.
+* Use `iso` or `≅` to refer to isomorphisms of types or structures.
   Here an isomorphism is a function with a quasi-inverse, i.e. a
   quasi-equivalence in the sense of the HoTT Book.
   Operators can use subscript `ᵢ`.
@@ -54,15 +62,14 @@ For naming conventions specific to the Algebra subfolder, see
 
 * Prefer using `→` over `to`.
 
--- TODO what's the good alternative?
 * Results about `PathP` (path overs) should end with `P` (like
-  `compPathP`).
+  `compP`).
 
 * Type families valued in propositions, either defined as records,
   functions or as truncated inductive types, should start with the word
   `is`: `is-prop`, `is-set`, etc. Predicates should be written _after_
   what they apply to: `Nat-is-set`, `is-prop-is-prop`,
-  `is-hlevel-is-prop`. Record fields indicating the truth of a predicate
+  `is-of-hlevel-is-prop`. Record fields indicating the truth of a predicate
   should be prefixed `has-is-`, since Agda doesn't allow you to shadow
   globals with record fields.
 

src/Data/Id.agda

@@ -82,7 +82,7 @@ opaque
   is-setⁱ→is-set A-setⁱ x y p q =
     let z = A-setⁱ x y (Id≃path.from p) (Id≃path.from q)
         w = apⁱ Id≃path.to z
-    in Id≃path.to (subst₂ _＝ⁱ_ (Id≃path.ε _) (Id≃path.ε _) w)
+    in Id≃path.to (subst² _＝ⁱ_ (Id≃path.ε _) (Id≃path.ε _) w)
 
 
 _on-pathsⁱ-of_ : (Type ℓ → Type ℓ′) → Type ℓ → Type (ℓ ⊔ ℓ′)

src/Data/List/Container.agda

@@ -30,7 +30,7 @@ container→list′ : (n : ℕ) (f : Fin n → A) → Listⁱ A
 container→list′ 0       _ = []
 container→list′ (suc n) f = f fzero ∷ container→list′ n (f ∘ fsuc)
 
-list→container→list : (xs : Listⁱ A) → container→list′ $₂ (list→container xs) ＝ xs
+list→container→list : (xs : Listⁱ A) → container→list′ $² (list→container xs) ＝ xs
 list→container→list []       = refl
 list→container→list (x ∷ xs) = ap (x ∷_) (list→container→list xs)
 
@@ -44,4 +44,4 @@ container→list→container (suc n) f =
 
 list-container-equiv : Listⁱ A ≃ List A
 list-container-equiv =
-  iso→equiv (list→container , iso (container→list′ $₂_) (container→list→container $₂_) list→container→list)
+  iso→equiv (list→container , iso (container→list′ $²_) (container→list→container $²_) list→container→list)

src/Data/List/Instances/Discrete.agda

@@ -22,7 +22,7 @@ list-is-discrete di = is-discrete-η go where
   go []       (_ ∷ _)  = no $ ∷≠[] ∘ sym
   go (_ ∷ _)  []       = no ∷≠[]
   go (x ∷ xs) (y ∷ ys) = Dec.map
-    (λ (x=y , xs=ys) → ap₂ _∷_ x=y xs=ys)
+    (λ (x=y , xs=ys) → ap² _∷_ x=y xs=ys)
     (λ f p → f (∷-head-inj p , ap tail p))
     (×-decision (is-discrete-β di x y) $ go xs ys)
 

src/Data/List/Path.agda

@@ -47,7 +47,7 @@ module List-path-code where
 
   decode : Code xs ys → xs ＝ ys
   decode {xs = []}     {([])}   _       = refl
-  decode {xs = x ∷ xs} {y ∷ ys} (p , c) = ap₂ _∷_ p (decode c)
+  decode {xs = x ∷ xs} {y ∷ ys} (p , c) = ap² _∷_ p (decode c)
 
   code-refl-pathP : {xs ys : List A} (c : Code xs ys) → ＜ code-refl xs ／ (λ i → Code xs (decode c i)) ＼ c ＞
   code-refl-pathP {xs = []}     {([])}   (lift tt) = refl

src/Data/Nat/Order/Inductive.agda

@@ -93,7 +93,7 @@ instance
 ≤-weak-+l x (suc y) z prf = ≤-suc-r (≤-weak-+l x y z prf)
 
 ≤-subst : {a b c d : ℕ} → a ＝ b → c ＝ d → a ≤ c → b ≤ d
-≤-subst ab cd = transport $ ap₂ (_≤_) ab cd
+≤-subst ab cd = transport $ ap² (_≤_) ab cd
 
 ≤-+l-≃ : {x y z : ℕ} → (y ≤ z) ≃ (x + y ≤ x + z)
 ≤-+l-≃ {x} {y} {z} = prop-extₑ! (ff x y z) (gg x y z)

src/Data/Nat/Properties.agda

@@ -71,7 +71,7 @@ open import Data.Nat.Path
 ·-distrib-+r (suc x) y z = ap (λ q → z + q) (·-distrib-+r x y z) ∙ +-assoc z (x · z) (y · z)
 
 ·-distrib-+l : (x y z : ℕ) → x · (y + z) ＝ x · y + x · z
-·-distrib-+l x y z = ·-comm x (y + z) ∙ ·-distrib-+r y z x ∙ ap₂ (_+_) (·-comm y x) (·-comm z x)
+·-distrib-+l x y z = ·-comm x (y + z) ∙ ·-distrib-+r y z x ∙ ap² (_+_) (·-comm y x) (·-comm z x)
 
 ·-assoc : (x y z : ℕ) → x · (y · z) ＝ x · y · z
 ·-assoc  zero   y z = refl

src/Data/Quotient/Set/Properties.agda

@@ -106,7 +106,7 @@ universal {B} {A} {R} B-set = iso→equiv $ inc , iso back (λ _ → refl) li wh
   instance _ = B-set
   inc : (A / R → B) → Σ[ f ꞉ (A → B) ] (∀ a b → R a b → f a ＝ f b)
   inc f = f ∘ ⦋_⦌ , λ a b r i → f (glue/ a b r i)
-  back = rec! $₂_
+  back = rec! $²_
   li : _
   li f′ = fun-ext λ r → ∥-∥₁.rec! (λ (_ , p) → ap (back (inc f′)) (sym p) ∙ ap f′ p) (⦋-⦌-surjective r)
 

src/Data/Tree/Binary/Path.agda

@@ -71,7 +71,7 @@ module tree-path-code {A : Type ℓ} where
   decode : Code xs ys → xs ＝ ys
   decode {xs = empty} {ys = empty} _ = refl
   decode {xs = leaf x} {ys = leaf y} = ap leaf
-  decode {xs = node xl xr} {ys = node yl yr} (p , q) = ap₂ node (decode p) (decode q)
+  decode {xs = node xl xr} {ys = node yl yr} (p , q) = ap² node (decode p) (decode q)
 
   code-refl-pathP : (c : Code xs ys) → ＜ code-refl xs ／ (λ i → Code xs (decode c i)) ＼ c ＞
   code-refl-pathP {xs = empty} {ys = empty} _ = refl

src/Data/Vec/Instances/Discrete.agda

@@ -21,7 +21,7 @@ vec-is-discrete {A} di = is-discrete-η go where
   go : ∀ {@0 n} → (xs ys : Vec A n) → Dec (xs ＝ ys)
   go []       []       = yes refl
   go (x ∷ xs) (y ∷ ys) = Dec.map
-    (λ (x=y , xs=ys) → ap₂ _∷_ x=y xs=ys)
+    (λ (x=y , xs=ys) → ap² _∷_ x=y xs=ys)
     (λ f p → f (ap head p , ap tail p))
     (×-decision (is-discrete-β di x y) $ go xs ys)
 

src/Foundations/Base.agda

@@ -77,23 +77,23 @@ apP : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ′}
 apP f p i = f i (p i)
 {-# INLINE apP #-}
 
-ap₂ : {C : Π[ a ꞉ A ] Π[ b ꞉ B a ] Type ℓ}
+ap² : {C : Π[ a ꞉ A ] Π[ b ꞉ B a ] Type ℓ}
       (f : Π[ a ꞉ A ] Π[ b ꞉ B a ] C a b)
       (p : x ＝ y) {u : B x} {v : B y}
       (q : ＜     u    ／ (λ i →          B (p i)) ＼        v ＞)
     →      ＜ f x u ／ (λ i    → C (p i) (q    i ))   ＼ f y v ＞
-ap₂ f p q i = f (p i) (q i)
-{-# INLINE ap₂ #-}
+ap² f p q i = f (p i) (q i)
+{-# INLINE ap² #-}
 
-apP₂ : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ′}
+apP² : {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ′}
        {C : (i : I) → Π[ a ꞉ A i ] (B i a → Type ℓ″)}
        (f : (i : I) → Π[ a ꞉ A i ] Π[ b ꞉ B i a ] C i a b)
        {x : A i0} {y : A i1} {u : B i0 x} {v : B i1 y}
        (p : ＜      x         ／ (λ i →      A i)          ＼            y   ＞)
        (q : ＜        u    ／ (λ i    →            B i (p i)) ＼           v ＞)
      →      ＜ f i0 x u ／ (λ i       → C i (p i) (q      i ))   ＼ f i1 y v ＞
-apP₂ f p q i = f i (p i) (q i)
-{-# INLINE apP₂ #-}
+apP² f p q i = f i (p i) (q i)
+{-# INLINE apP² #-}
 
 {- Observe an "open box".
 

src/Foundations/HLevel/Retracts.agda

@@ -54,9 +54,9 @@ opaque
       inv : sect is-left-inverse-of (ap g)
       inv path =
         sym (p x) ∙ ap f (ap g path) ∙ p y ∙ refl ＝⟨ ap (λ e → sym (p _) ∙ _ ∙ e) (∙-id-r (p _)) ⟩
-        sym (p x) ∙ ap f (ap g path) ∙ p y        ＝⟨ ap₂ _∙_ refl (sym (homotopy-natural p _)) ⟩
+        sym (p x) ∙ ap f (ap g path) ∙ p y        ＝⟨ ap² _∙_ refl (sym (homotopy-natural p _)) ⟩
         sym (p x) ∙ p x ∙ path                    ＝⟨ ∙-assoc _ _ _ ⟩
-        (sym (p x) ∙ p x) ∙ path                  ＝⟨ ap₂ _∙_ (∙-inv-l (p x)) refl ⟩
+        (sym (p x) ∙ p x) ∙ path                  ＝⟨ ap² _∙_ (∙-inv-l (p x)) refl ⟩
         refl ∙ path                               ＝⟨ ∙-id-l path ⟩
         path                                      ∎
 

src/Foundations/Pi/Properties.agda

@@ -29,7 +29,7 @@ private variable
     .fst k x → k (e .fst x)
     .snd .is-iso.inv k x → subst P (ε x) (k (from x))
     .snd .is-iso.rinv k → fun-ext λ x →
-        ap₂ (subst P) (sym (zig x))
+        ap² (subst P) (sym (zig x))
           (sym (from-pathP (symP-from-goal (ap k (η x)))))
       ∙ transport⁻-transport (ap P (ap to (sym (η x)))) (k x)
     .snd .is-iso.linv k → fun-ext λ x →

src/Foundations/Sigma/Base.agda

@@ -56,28 +56,28 @@ second : {C : A → Type ℓ‴} → (∀ {x} → B x → C x) → Σ A B → Σ
 second f = bimap (λ x → x) f
 
 
-_$₂_ : (f : (a : A) (b : B a) → C a b)
+_$²_ : (f : (a : A) (b : B a) → C a b)
        (p : Σ[ x ꞉ A ] B x)
      → C (fst p) (snd p)
-f $₂ (x , y) = f x y
+f $² (x , y) = f x y
 
--- TODO: automate this to get `curryₙ` and `uncurryₙ` (`_$ₙ_`)
-_$₃_ : (f : (a : A) (b : B a) (c : C a b) → D a b c)
+-- TODO: automate this to get `curryⁿ` and `uncurryⁿ` (`_$ⁿ_`)
+_$³_ : (f : (a : A) (b : B a) (c : C a b) → D a b c)
        (p : Σ[ x ꞉ A ] Σ[ y ꞉ B x ] C x y)
      → D (p .fst) (p .snd .fst) (p .snd .snd)
-f $₃ (x , y , z) = f x y z
+f $³ (x , y , z) = f x y z
 
-_$₄_ : (f : (a : A) (b : B a) (c : C a b) (d : D a b c) → E a b c d)
+_$⁴_ : (f : (a : A) (b : B a) (c : C a b) (d : D a b c) → E a b c d)
        (p : Σ[ x ꞉ A ] Σ[ y ꞉ B x ] Σ[ z ꞉ C x y ] D x y z)
      → E (p .fst) (p .snd .fst) (p .snd .snd .fst) (p .snd .snd .snd)
-f $₄ (x , y , z , w) = f x y z w
+f $⁴ (x , y , z , w) = f x y z w
 
-_$₅_ : (f : (a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → F a b c d e)
+_$⁵_ : (f : (a : A) (b : B a) (c : C a b) (d : D a b c) (e : E a b c d) → F a b c d e)
        (p : Σ[ x ꞉ A ] Σ[ y ꞉ B x ] Σ[ z ꞉ C x y ] Σ[ w ꞉ D x y z ] E x y z w)
      → F (p .fst) (p .snd .fst) (p .snd .snd .fst) (p .snd .snd .snd .fst) (p .snd .snd .snd .snd)
-f $₅ (x , y , z , w , u) = f x y z w u
+f $⁵ (x , y , z , w , u) = f x y z w u
 
--- note that `curry₁` is just `_$_`
+-- note that `curry¹` is just `_$_`
 
 curry₂ : (f : (p : Σ[ a ꞉ A ] B a) → C (p .fst) (p .snd))
          (x : A) (y : B x) → C x y

src/Foundations/Sigma/Properties.agda

@@ -57,8 +57,8 @@ open is-iso
   morp : Σ _ P ≅ Σ _ Q
   morp .fst (i , x) = i , pointwise i .fst x
   morp .snd .inv (i , x) = i , pwise i .snd .inv x
-  morp .snd .rinv (i , x) = ap₂ _,_ refl (pwise i .snd .rinv _)
-  morp .snd .linv (i , x) = ap₂ _,_ refl (pwise i .snd .linv _)
+  morp .snd .rinv (i , x) = ap² _,_ refl (pwise i .snd .rinv _)
+  morp .snd .linv (i , x) = ap² _,_ refl (pwise i .snd .linv _)
 
 Σ-ap-fst : (e : A ≃ A′) → Σ A (B ∘ e .fst) ≃ Σ A′ B
 Σ-ap-fst {A} {A′} {B} e = intro , intro-is-equiv

src/Foundations/Transport.agda

@@ -50,14 +50,14 @@ subst⁻-subst : (B : A → Type ℓ′) (p : x ＝ y)
 subst⁻-subst B p u = transport⁻-transport (ap B p) u
 
 
-subst₂ : {B : Type ℓ′} {z w : B} (C : A → B → Type ℓ″)
+subst² : {B : Type ℓ′} {z w : B} (C : A → B → Type ℓ″)
          (p : x ＝ y) (q : z ＝ w) → C x z → C y w
-subst₂ B p q = transport (λ i → B (p i) (q i))
+subst² B p q = transport (λ i → B (p i) (q i))
 
-subst₂-filler : {B : Type ℓ′} {z w : B} (C : A → B → Type ℓ″)
+subst²-filler : {B : Type ℓ′} {z w : B} (C : A → B → Type ℓ″)
                 (p : x ＝ y) (q : z ＝ w) (c : C x z)
-              → ＜ c ／ (λ i → C (p i) (q i)) ＼ subst₂ C p q c ＞
-subst₂-filler C p q = transport-filler (ap₂ C p q)
+              → ＜ c ／ (λ i → C (p i) (q i)) ＼ subst² C p q c ＞
+subst²-filler C p q = transport-filler (ap² C p q)
 
 subst-comp : (B : A → Type ℓ′)
            → (p : x ＝ y) (q : y ＝ z) (u : B x)

src/Functions/Equiv/HalfAdjoint.agda

@@ -54,7 +54,7 @@ fibre-paths {f} {y} {f1} {f2} =
            →  (subst (λ x → f x ＝ y) refl (f1 .snd) ＝ p′)
            ＝ (ap f refl ∙ p′ ＝ f1 .snd)
     helper p′ =
-      subst (λ x → f x ＝ y) refl (f1 .snd) ＝ p′ ＝⟨ ap₂ _＝_ (transport-refl _) refl ⟩
+      subst (λ x → f x ＝ y) refl (f1 .snd) ＝ p′ ＝⟨ ap² _＝_ (transport-refl _) refl ⟩
       (f1 .snd) ＝ p′                             ＝⟨ iso→path (sym , iso sym (λ x → refl) (λ x → refl)) ⟩
       ⌜ p′ ⌝ ＝ f1 .snd                           ＝˘⟨ ap¡ (∙-id-l _) ⟩
       refl ∙ p′ ＝ f1 .snd                        ＝⟨⟩
@@ -81,7 +81,7 @@ is-half-adjoint-equiv→is-equiv {A} {B} {f} (g , η , ε , zig) .equiv-proof y
 
     path : ap f (ap g (sym p) ∙ η x) ∙ p ＝ ε y
     path =
-      ap f (ap g (sym p) ∙ η x) ∙ p                   ＝⟨ ap₂ _∙_ (ap-comp-∙ f (ap g (sym p)) (η x)) refl ∙ sym (∙-assoc _ _ _) ⟩
+      ap f (ap g (sym p) ∙ η x) ∙ p                   ＝⟨ ap² _∙_ (ap-comp-∙ f (ap g (sym p)) (η x)) refl ∙ sym (∙-assoc _ _ _) ⟩
       ap (λ x → f (g x)) (sym p) ∙ ⌜ ap f (η x) ⌝ ∙ p ＝⟨ ap! (zig _) ⟩ -- by the triangle identity
       ap (f ∘ g) (sym p) ∙ ⌜ ε (f x) ∙ p ⌝            ＝⟨ ap! (homotopy-natural ε p)  ⟩ -- by naturality of ε
       ap (f ∘ g) (sym p) ∙ ap (f ∘ g) p ∙ ε y         ＝⟨ ∙-assoc _ _ _ ⟩

src/Functions/Equiv/Weak.agda

@@ -25,5 +25,5 @@ is-surjective-embedding→is-equiv sur emb .equiv-proof y =
 
 is-surjective-embedding≃is-equiv : is-surjective f × is-embedding f ≃ is-equiv f
 is-surjective-embedding≃is-equiv = prop-extₑ!
-  (is-surjective-embedding→is-equiv $₂_)
+  (is-surjective-embedding→is-equiv $²_)
   (λ fe → is-equiv→is-surjective fe , is-equiv→is-embedding fe)

src/Order/Base.agda

@@ -22,7 +22,7 @@ record is-partial-order {ℓ ℓ′} {A : Type ℓ}
     has-is-set : is-set A
     has-is-set = identity-system→hlevel 1
       {r = λ _ → ≤-refl , ≤-refl}
-      (set-identity-system hlevel! (≤-antisym $₂_))
+      (set-identity-system hlevel! (≤-antisym $²_))
       hlevel!