fix naming in Nat.Order so that the name of lemmas don't include any free varibles (#1319)

Author: LorenzoMolena

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

@@ -487,7 +487,7 @@ snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHo
   where
     sum→product : (ℤ[Fin (n +ℕ m) ] .fst) → ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst)
     sum→product x = ((λ (a , Ha) → x (a , <→<ᵗ (≤-trans (<ᵗ→< Ha) (≤SumLeft {n}{m}))))
-                    , λ (a , Ha) → x (n +ℕ a , <→<ᵗ (<-k+ {a}{m}{n} (<ᵗ→< Ha))))
+                    , λ (a , Ha) → x (n +ℕ a , <→<ᵗ (<-+ˡ {a}{m}{n} (<ᵗ→< Ha))))
 
     product→sum : ((AbDirProd ℤ[Fin n ] ℤ[Fin m ]) .fst) → (ℤ[Fin (n +ℕ m) ] .fst)
     product→sum (x , y) (a , Ha) with (a ≟ᵗ n)
@@ -506,7 +506,7 @@ snd (sumCoefficients n) = makeIsGroupHom (λ x y → funExt λ _ → sumFinℤHo
 
         lemy : (a : ℕ) (Ha : a <ᵗ m) → snd (sum→product (product→sum (x , y))) (a , Ha) ≡ y (a , Ha)
         lemy a Ha with ((n +ℕ a) ≟ᵗ n)
-        ... | lt H = rec (¬m<m (≤<-trans (≤SumLeft {n}{a}) (<ᵗ→< H)))
+        ... | lt H = rec (<-irrefl (≤<-trans (≤SumLeft {n}{a}) (<ᵗ→< H)))
         ... | eq H = cong y (Fin≡ _ _ (∸+ a n))
         ... | gt H = cong y (Fin≡ _ _ (∸+ a n))
 

Cubical/Algebra/DirectSum/DirectSumFun/Properties.agda

@@ -47,7 +47,7 @@ module DSF-properties
     Anf+g = PT.rec2 squash₁
             (λ { (k , nf) → λ { (l , ng) →
                ∣ ((k +n l) ,
-                 (λ n p → cong₂ ((Gstr n)._+_) (nf n (<-+k-trans p)) (ng n (<-k+-trans p))
+                 (λ n p → cong₂ ((Gstr n)._+_) (nf n (<-+-transʳ p)) (ng n (<-+-transˡ p))
                            ∙ +IdR (Gstr n) (0g (Gstr n)))) ∣₁ } })
 
 

Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda

@@ -173,7 +173,7 @@ module Equiv-Properties
                       λ {U} {V} → PT.elim (λ _ → isPropΠ (λ _ → squash₁))
                                    (λ { (k , nu) → PT.elim (λ _ → squash₁)
                                     λ { (l , nv) →
-                                   ∣ ((k +n l) , (λ n q → cong₂ ((Gstr n)._+_) (nu n (<-+k-trans q)) (nv n (<-k+-trans q))
+                                   ∣ ((k +n l) , (λ n q → cong₂ ((Gstr n)._+_) (nu n (<-+-transʳ q)) (nv n (<-+-transˡ q))
                                                           ∙ +IdR (Gstr n) _)) ∣₁} })
 
   ---------------------------------------------------------------------------

Cubical/Algebra/GradedRing/DirectSumFun.agda

@@ -152,7 +152,7 @@ module _
       where
       sumF0 : (i n : ℕ) → (pp : k +ℕ l < n) → (r : i ≤ n) → sumFun i n r f g ≡ 0g (Gstr n)
       sumF0 zero n pp r = cong (subst G (sameFiber r))
-                               (cong (λ X → f 0 ⋆ X) (ng (n -ℕ zero) (<-k+-trans pp)) ∙ ⋆-0 _) ∙ substG0 _
+                               (cong (λ X → f 0 ⋆ X) (ng (n -ℕ zero) (<-+-transˡ pp)) ∙ ⋆-0 _) ∙ substG0 _
       sumF0 (suc i) n pp r with splitℕ-≤ (suc i) k
       ... | inl x = cong₂ (Gstr n ._+_)
                         (cong (subst G (sameFiber r))
@@ -161,7 +161,7 @@ module _
                                     -- Proof : l = k + l - k < n - k < n - suc i
                                     (subst (λ X → X < n -ℕ suc i) (∸+ l k)
                                             (≤<-trans (≤-∸-≥ (k +ℕ l) (suc i) k x)
-                                            (<-∸-< (k +ℕ l) n (suc i) pp (≤<-trans x (<-+k-trans pp))))))
+                                            (<-∸-< (k +ℕ l) n (suc i) pp (≤<-trans x (<-+-transʳ pp))))))
                               ∙ ⋆-0 (f (suc i))))
                         (sumF0 i n pp (≤-trans ≤-sucℕ r))
                   ∙ +IdR (Gstr n) _

Cubical/Algebra/OrderedCommMonoid/Instances.agda

@@ -17,7 +17,7 @@ open import Cubical.Data.Nat.Order
          isSetℕ
          +-assoc +-zero (λ _ → refl) +-comm
          (λ _ _ → isProp≤) (λ _ → ≤-refl) (λ _ _ _ → ≤-trans) (λ _ _ → ≤-antisym)
-         (λ _ _ _ → ≤-+k) (λ _ _ _ → ≤-k+)
+         (λ _ _ _ → ≤-+ʳ) (λ _ _ _ → ≤-+ˡ)
 
 ℕ≤· : OrderedCommMonoid ℓ-zero ℓ-zero
 ℕ≤· .fst = ℕ
@@ -29,6 +29,6 @@ open import Cubical.Data.Nat.Order
         isSetℕ
         ·-assoc ·-identityʳ ·-identityˡ ·-comm
         (λ _ _ → isProp≤) (λ _ → ≤-refl) (λ _ _ _ → ≤-trans) (λ _ _ → ≤-antisym)
-        (λ _ _ _ → ≤-·k) lmono
+        (λ _ _ _ → ≤-·ʳ) lmono
   where lmono : (x y z : ℕ) → x ≤ y → z · x ≤ z · y
-        lmono x y z x≤y = subst ((z · x) ≤_) (·-comm y z) (subst (_≤ (y · z)) (·-comm x z) (≤-·k x≤y))
+        lmono x y z x≤y = subst ((z · x) ≤_) (·-comm y z) (subst (_≤ (y · z)) (·-comm x z) (≤-·ʳ x≤y))

Cubical/CW/Connected.agda

@@ -1315,8 +1315,8 @@ makeConnectedCW {ℓ = ℓ} (suc n) {C = C} (cwsk , eqv) cA with
             C'-realise : (n₁ : ℕ) (q : _)
               → Iso (C' (n₁ +ℕ 4+n) q)
                      (C* (n₁ +ℕ 4+n))
-            C'-realise m (lt x) = ⊥.rec (¬m<m (<-trans (<ᵗ→< x) (m , refl)))
-            C'-realise m (eq x) = ⊥.rec (¬m<m (m , x))
+            C'-realise m (lt x) = ⊥.rec (<-irrefl (<-trans (<ᵗ→< x) (m , refl)))
+            C'-realise m (eq x) = ⊥.rec (<-irrefl (m , x))
             C'-realise zero (gt x) = idIso
             C'-realise (suc m) (gt x) = idIso
 
@@ -1326,8 +1326,8 @@ makeConnectedCW {ℓ = ℓ} (suc n) {C = C} (cwsk , eqv) cA with
                       (Iso.fun (C'-realise n₁ q) a)
                 ≡ Iso.fun (C'-realise (suc n₁) _)
                     (invEq (e' (n₁ +ℕ 4+n) r q) (inl a))
-            C'-realise-coh m (lt x) r a = ⊥.rec (¬m<m (<-trans (<ᵗ→< x) (m , refl)))
-            C'-realise-coh m (eq x) r a = ⊥.rec (¬m<m (m , x))
+            C'-realise-coh m (lt x) r a = ⊥.rec (<-irrefl (<-trans (<ᵗ→< x) (m , refl)))
+            C'-realise-coh m (eq x) r a = ⊥.rec (<-irrefl (m , x))
             C'-realise-coh m (gt x) (lt x₁) a =
               ⊥.rec (¬m<ᵗm (<ᵗ-trans (<ᵗ-trans x x₁) <ᵗsucm))
             C'-realise-coh m (gt x) (eq x₁) a =

Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda

@@ -308,7 +308,7 @@ module _ (G : AbGroup ℓ) where
   snd (Hⁿ[Sᵐ,G]Full zero  m) p = ⊥.rec (fst p refl)
   Hⁿ[Sᵐ,G]Full  (suc n) m with (n ≟ m)
   ... | lt x = (λ { (inl x) → ⊥.rec (snotz x)
-                  ; (inr p) → ⊥.rec (¬m<m (subst (n <_) (sym (cong predℕ p)) x))})
+                  ; (inr p) → ⊥.rec (<-irrefl (subst (n <_) (sym (cong predℕ p)) x))})
              , λ _ → subst (λ m → AbGroupEquiv (coHomGr (suc n) G (S₊ m))
                                                  (trivialAbGroup {ℓ-zero}))
                             (cong suc (snd x))
@@ -320,7 +320,7 @@ module _ (G : AbGroup ℓ) where
                             (Hⁿ[Sⁿ,G]≅G n)})
     , (λ p → ⊥.rec (p .snd (cong suc x)))
   ... | gt x = (λ { (inl x) → ⊥.rec (snotz x)
-                  ; (inr p) → ⊥.rec (¬m<m (subst (m <_) (cong predℕ p) x))})
+                  ; (inr p) → ⊥.rec (<-irrefl (subst (m <_) (cong predℕ p) x))})
              , λ _ → subst (λ n → AbGroupEquiv (coHomGr n G (S₊ (suc m)))
                                                  (trivialAbGroup {ℓ-zero}))
                             (cong suc (snd x))

Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda

@@ -345,7 +345,7 @@ module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where
       → H*[Sⁿ,G]→G[X]/<X²>-fun^ n p
            (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g)
        ≡ [ base (one ∷ []) g ]
-    h2 g (lt x) = ⊥.rec (¬m<m x)
+    h2 g (lt x) = ⊥.rec (<-irrefl x)
     h2 g (eq x) = cong [_]
       (cong (base (1 ∷ []))
         (cong (Hⁿ[Sⁿ,G]≅G GAb n .fst .fst)
@@ -354,7 +354,7 @@ module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where
                   (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g))
         ∙ transportRefl (invEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g))
         ∙ secEq (Hⁿ[Sⁿ,G]≅G GAb n .fst) g))
-    h2 g (gt x) = ⊥.rec (¬m<m x)
+    h2 g (gt x) = ⊥.rec (<-irrefl x)
 
 
   G[X]/<X²>≅H*[Sⁿ,G] : RingEquiv (CommRing→Ring G[X]/<X²>) (H*R GRing (S₊ (suc n)))

Cubical/Data/Fin/Properties.agda

@@ -453,9 +453,9 @@ factorEquiv {suc n} {m} = intro , isEmbedding×isSurjection→isEquiv (isEmbeddi
     mm<m = <ᵗ→< (snd mm)
     nm<n·m : toℕ {k = m} mm · suc n + toℕ {k = suc n} nn < suc n · m
     nm<n·m =
-      toℕ {k = m} mm · suc n + toℕ {k = suc n} nn   <≤⟨ <-k+ nn< ⟩
+      toℕ {k = m} mm · suc n + toℕ {k = suc n} nn   <≤⟨ <-+ˡ nn< ⟩
       toℕ {k = m} mm · suc n + suc n                ≡≤⟨ +-comm (toℕ {k = m} mm · suc n) (suc n) ⟩
-      suc (toℕ {k = m} mm) · suc n                  ≤≡⟨ ≤-·k mm<m ⟩
+      suc (toℕ {k = m} mm) · suc n                  ≤≡⟨ ≤-·ʳ mm<m ⟩
       m · suc n                                     ≡⟨ sym (·-comm (suc n) m) ⟩
       suc n · m                                     ∎ where open <-Reasoning
 
@@ -492,7 +492,7 @@ factorEquiv {suc n} {m} = intro , isEmbedding×isSurjection→isEquiv (isEmbeddi
       m · suc n       ∎ where open <-Reasoning
 
     mm<m : mm < m
-    mm<m = <-·sk-cancel mm·sn<m·sn
+    mm<m = <-·-cancelʳ mm·sn<m·sn
     nnFin : Fin (suc n)
     nnFin = nn , n%sk<ᵗsk k _
     mmFin : Fin m
@@ -560,15 +560,15 @@ Iso.inv (Fin+≅Fin⊎Fin m n) = g
   where
     g :  Fin m  ⊎  Fin n  →  Fin (m + n)
     g (inl (k , k<m)) = k     , <→<ᵗ (o<m→o<m+n m n k (<ᵗ→< k<m))
-    g (inr (k , k<n)) = m + k , <→<ᵗ (<-k+ {k = m} (<ᵗ→< k<n))
+    g (inr (k , k<n)) = m + k , <→<ᵗ (<-+ˡ {k = m} (<ᵗ→< k<n))
 Iso.sec (Fin+≅Fin⊎Fin m n) = sec-f-g
   where
     sec-f-g : _
     sec-f-g (inl (k , k<m)) with k ≤? m
     sec-f-g (inl (k , k<m)) | inl _   = cong inl (Σ≡Prop (λ z → isProp<ᵗ {n = z} {m = m}) refl)
     sec-f-g (inl (k , k<m)) | inr m≤k = Empty.rec (¬-<-and-≥ (<ᵗ→< k<m) m≤k)
     sec-f-g (inr (k , k<n)) with (m + k) ≤? m
-    sec-f-g (inr (k , k<n)) | inl p   = Empty.rec (¬m+n<m {m} {k} p)
+    sec-f-g (inr (k , k<n)) | inl p   = Empty.rec (¬SumLeft< {m} {k} p)
     sec-f-g (inr (k , k<n)) | inr k≥m = cong inr (Σ≡Prop (λ z → isProp<ᵗ {n = z} {m = n}) rem)
       where
         rem : (m + k) ∸ m ≡ k
@@ -749,21 +749,21 @@ module _ (_+A_ : A → A → A) (0A : A)
     sumFin-choose {zero} f a x p t = Empty.rec (¬Fin0 x)
     sumFin-choose {suc n} f a x p t with (n ≟ fst x)
     ... | lt x₁ =
-      Empty.rec (¬m<m {suc n} ((fst (<ᵗ→< {n = x .fst} {suc n} (x .snd))) + fst x₁
+      Empty.rec (<-irrefl {suc n} ((fst (<ᵗ→< {n = x .fst} {suc n} (x .snd))) + fst x₁
            , (sym (+-assoc (fst (<ᵗ→< {n = x .fst} {suc n} (x .snd))) (fst x₁) (suc (suc n)))
            ∙ (cong (fst (<ᵗ→< {n = x .fst} {suc n} (x .snd)) +_ ) (+-suc (fst x₁) (suc n))))
            ∙ sym ((sym (<ᵗ→< {n = x .fst} (x .snd) .snd))
                 ∙ cong (fst (<ᵗ→< {n = x .fst} {suc n} ((x .snd))) +_) (sym (cong suc (x₁ .snd))))))
     ... | eq x₁ =
       cong (f flast +A_) (sumFinGen0 n _
-        λ h → t _ λ q → ¬m<m (subst (_< n) (cong fst q ∙ sym x₁) (<ᵗ→< (h .snd))))
+        λ h → t _ λ q → <-irrefl (subst (_< n) (cong fst q ∙ sym x₁) (<ᵗ→< (h .snd))))
              ∙ rUnit _ ∙ sym (cong f x=flast) ∙ p
       where
       x=flast : x ≡ flast
       x=flast = Σ≡Prop (λ z → isProp<ᵗ {n = z} {m = suc n}) (sym x₁)
     ... | gt x₁ =
       cong₂ _+A_
-         (t flast (λ p → ¬m<m (subst (_< n) (sym (cong fst p)) x₁)))
+         (t flast (λ p → <-irrefl (subst (_< n) (sym (cong fst p)) x₁)))
          refl
       ∙ lUnitA _
       ∙ sumFin-choose {n = n} (f ∘ injectSuc) a (fst x , <→<ᵗ x₁)

Cubical/Data/FinData/Properties.agda

@@ -276,7 +276,7 @@ enumElim P k p h f i =
 -- ++Fin is commutative, but how to go from there?
 +Shuffle : (m n : ℕ) → Fin (m + n) → Fin (n + m)
 +Shuffle m n i with <Dec (toℕ i) m
-... | yes i<m = toFin (n + (toℕ i)) (<-k+ i<m)
+... | yes i<m = toFin (n + (toℕ i)) (<-+ˡ i<m)
 ... | no ¬i<m = toFin (toℕ i ∸ m)
                   (subst (λ x → toℕ i ∸ m < x) (+-comm m n) (≤<-trans (∸-≤ (toℕ i) m) (toℕ<n i)))