Resolve naming inconsistency between Iso and Category.isIso

Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda

@@ -82,12 +82,12 @@ module _ {A : Type ℓ} where
     AbelienizeFreeGroup→FreeAbGroup .fst
   Iso.inv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
     FreeAbGroup→AbelienizeFreeGroup .fst
-  Iso.rightInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) x i =
+  Iso.sec (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) x i =
     FAGAbGroupGroupHom≡
       (compGroupHom FreeAbGroup→AbelienizeFreeGroup
                     AbelienizeFreeGroup→FreeAbGroup)
       idGroupHom (λ _ → refl) i .fst x
-  Iso.leftInv (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
+  Iso.ret (fst GroupIso-AbelienizeFreeGroup→FreeAbGroup) =
     Abi.elimProp _ (λ _ → isset _ _)
     (funExt⁻ (cong fst (freeGroupHom≡
       {f = compGroupHom  freeGroup→freeAbGroup FreeAbGroup→AbelienizeFreeGroup}
@@ -387,8 +387,8 @@ Free→ℤFin→Free (suc n) =
 Iso-ℤFin-FreeAbGroup : (n : ℕ) → Iso (ℤ[Fin n ] .fst) (FAGAbGroup {A = Fin n} .fst)
 Iso.fun (Iso-ℤFin-FreeAbGroup n) = ℤFin→Free n
 Iso.inv (Iso-ℤFin-FreeAbGroup n) = Free→ℤFin n
-Iso.rightInv (Iso-ℤFin-FreeAbGroup n) = ℤFin→Free→ℤFin n
-Iso.leftInv (Iso-ℤFin-FreeAbGroup n) = Free→ℤFin→Free n
+Iso.sec (Iso-ℤFin-FreeAbGroup n) = ℤFin→Free→ℤFin n
+Iso.ret (Iso-ℤFin-FreeAbGroup n) = Free→ℤFin→Free n
 
 ℤFin≅FreeAbGroup : (n : ℕ) → AbGroupIso (ℤ[Fin n ]) (FAGAbGroup {A = Fin n})
 fst (ℤFin≅FreeAbGroup n) = Iso-ℤFin-FreeAbGroup n
@@ -404,7 +404,7 @@ elimPropℤFin : ∀ {ℓ} (n : ℕ)
   → ((f : _) → A f → A (-ℤ_ ∘ f))
   → (x : _) → A x
 elimPropℤFin n A pr z t s u w =
-  subst A (Iso.leftInv (Iso-ℤFin-FreeAbGroup n) w) (help (ℤFin→Free n w))
+  subst A (Iso.ret (Iso-ℤFin-FreeAbGroup n) w) (help (ℤFin→Free n w))
   where
   help : (x : _) → A (Free→ℤFin n x)
   help = ElimProp.f (pr _) t z

Cubical/Algebra/AbGroup/Instances/IntMod.agda

@@ -44,8 +44,8 @@ Iso.inv (fst ℤ/2[2]≅ℤ/2) x = x , cong (x +ₘ_) (+ₘ-rUnit x) ∙ x+x x
   where
   x+x : (x : ℤ/2 .fst) → x +ₘ x ≡ fzero
   x+x = ℤ/2-elim refl refl
-Iso.rightInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl
-Iso.leftInv (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl
+Iso.sec (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isProp≤) refl
+Iso.ret (fst ℤ/2[2]≅ℤ/2) x = Σ≡Prop (λ _ → isSetFin _ _) refl
 snd ℤ/2[2]≅ℤ/2 = makeIsGroupHom λ _ _ → refl
 
 ℤ/2/2≅ℤ/2 : AbGroupIso (ℤ/2 /^ 2) ℤ/2
@@ -64,8 +64,8 @@ Iso.fun (fst ℤ/2/2≅ℤ/2) =
            λ p → ⊥.rec (snotz (sym (cong fst p))))))
           λ _ → refl)
 Iso.inv (fst ℤ/2/2≅ℤ/2) = [_]
-Iso.rightInv (fst ℤ/2/2≅ℤ/2) _ = refl
-Iso.leftInv (fst ℤ/2/2≅ℤ/2) =
+Iso.sec (fst ℤ/2/2≅ℤ/2) _ = refl
+Iso.ret (fst ℤ/2/2≅ℤ/2) =
   SQ.elimProp (λ _ → squash/ _ _) λ _ → refl
 snd ℤ/2/2≅ℤ/2 = makeIsGroupHom
   (SQ.elimProp (λ _ → isPropΠ λ _ → isSetFin _ _)

Cubical/Algebra/AbGroup/TensorProduct.agda

@@ -360,9 +360,9 @@ module UP (AGr : AbGroup ℓ) (BGr : AbGroup ℓ') where
                   (GroupHom (AGr *) (HomGroup (BGr *) C *))
     Iso.fun mainIso = _
     Iso.inv mainIso = invF
-    Iso.rightInv mainIso (f , p) = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
+    Iso.sec mainIso (f , p) = Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                                    (funExt λ a → Σ≡Prop (λ _ → isPropIsGroupHom _ _) refl)
-    Iso.leftInv mainIso (f , p) =
+    Iso.ret mainIso (f , p) =
         Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                 (funExt (⊗elimProp (λ _ → is-set (snd C) _ _)
                                    (λ _ _ → refl)
@@ -407,8 +407,8 @@ commFun²≡id = ⊗elimProp (λ _ → ⊗squash _ _)
           → GroupIso ((A ⨂ B) *) ((B ⨂ A) *)
 Iso.fun (fst ⨂-commIso) = commFun
 Iso.inv (fst ⨂-commIso) = commFun
-Iso.rightInv (fst ⨂-commIso) = commFun²≡id
-Iso.leftInv (fst ⨂-commIso) = commFun²≡id
+Iso.sec (fst ⨂-commIso) = commFun²≡id
+Iso.ret (fst ⨂-commIso) = commFun²≡id
 snd ⨂-commIso = makeIsGroupHom λ x y → refl
 
 ⨂-comm : ∀ {ℓ ℓ'} {A : AbGroup ℓ} {B : AbGroup ℓ'} → AbGroupEquiv (A ⨂ B) (B ⨂ A)
@@ -478,7 +478,7 @@ module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGr
   ⨂assocIso : Iso (A ⨂₁ (B ⨂ C)) ((A ⨂ B) ⨂₁ C)
   Iso.fun ⨂assocIso = fst assocHom⁻
   Iso.inv ⨂assocIso = fst assocHom
-  Iso.rightInv ⨂assocIso =
+  Iso.sec ⨂assocIso =
     ⊗elimProp (λ _ → ⊗squash _ _)
                (⊗elimProp (λ _ → isPropΠ (λ _ → ⊗squash _ _))
                            (λ a b c → refl)
@@ -487,7 +487,7 @@ module _ {ℓ ℓ' ℓ'' : Level} {A : AbGroup ℓ} {B : AbGroup ℓ'} {C : AbGr
                 λ x y p q → cong (fst assocHom⁻) (IsGroupHom.pres· (snd assocHom) x y)
                              ∙∙ IsGroupHom.pres· (snd assocHom⁻) (fst assocHom x) (fst assocHom y)
                              ∙∙ cong₂ _+⊗_ p q
-  Iso.leftInv ⨂assocIso =
+  Iso.ret ⨂assocIso =
     ⊗elimProp (λ _ → ⊗squash _ _)
                (λ a → ⊗elimProp (λ _ → ⊗squash _ _)
                                   (λ b c → refl)

Cubical/Algebra/Algebra/Properties.agda

@@ -174,14 +174,14 @@ module AlgebraEquivs where
       isoOnHoms : Iso (AlgebraHom B C) (AlgebraHom A C)
       fun isoOnHoms g = g ∘a AlgebraEquiv→AlgebraHom f
       inv isoOnHoms h = h ∘a AlgebraEquiv→AlgebraHom f⁻¹
-      rightInv isoOnHoms h =
+      sec isoOnHoms h =
         Σ≡Prop
           (λ h → isPropIsAlgebraHom _ (A .snd) h (C .snd))
-          (isoOnTypes .rightInv (h .fst))
-      leftInv isoOnHoms g =
+          (isoOnTypes .sec (h .fst))
+      ret isoOnHoms g =
         Σ≡Prop
           (λ g → isPropIsAlgebraHom _ (B .snd) g (C .snd))
-          (isoOnTypes .leftInv (g .fst))
+          (isoOnTypes .ret (g .fst))
 
 isSetAlgebraStr : (A : Type ℓ') → isSet (AlgebraStr R A)
 isSetAlgebraStr A =

Cubical/Algebra/ChainComplex/Homology.agda

@@ -136,15 +136,15 @@ module _ where
     finChainComplexMap→HomologyMap m f n .fst
   Iso.inv (fst (finChainComplexEquiv→HomoglogyIso m f n)) =
     finChainComplexMap→HomologyMap m (invFinChainMap f) n .fst
-  Iso.rightInv (fst (finChainComplexEquiv→HomoglogyIso m (f , eqs) n)) =
+  Iso.sec (fst (finChainComplexEquiv→HomoglogyIso m (f , eqs) n)) =
     funExt⁻ (cong fst (sym (finChainComplexMap→HomologyMapComp
                              (invFinChainMap (f , eqs)) f n))
            ∙∙  cong (λ f → fst (finChainComplexMap→HomologyMap m f n))
                  (finChainComplexMap≡ λ r
                    →  Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                                (funExt (secEq (_ , eqs r))))
            ∙∙ cong fst (finChainComplexMap→HomologyMapId n))
-  Iso.leftInv (fst (finChainComplexEquiv→HomoglogyIso m (f , eqs) n)) =
+  Iso.ret (fst (finChainComplexEquiv→HomoglogyIso m (f , eqs) n)) =
     funExt⁻ (cong fst (sym (finChainComplexMap→HomologyMapComp f
                             (invFinChainMap (f , eqs)) n))
           ∙∙ cong (λ f → fst (finChainComplexMap→HomologyMap m f n))
@@ -264,7 +264,7 @@ module _ where
     chainComplexMap→HomologyMap f n .fst
   Iso.inv (fst (chainComplexEquiv→HomoglogyIso (f , eqs) n)) =
     chainComplexMap→HomologyMap (invChainMap (f , eqs)) n .fst
-  Iso.rightInv (fst (chainComplexEquiv→HomoglogyIso (f , eqs) n)) =
+  Iso.sec (fst (chainComplexEquiv→HomoglogyIso (f , eqs) n)) =
     funExt⁻ (cong fst (sym (chainComplexMap→HomologyMapComp
                              (invChainMap (f , eqs)) f n))
            ∙∙  cong (λ f → fst (chainComplexMap→HomologyMap f n))
@@ -273,7 +273,7 @@ module _ where
                                (funExt (secEq (_ , eqs r))))
            ∙∙ cong fst (chainComplexMap→HomologyMapId n))
 
-  Iso.leftInv (fst (chainComplexEquiv→HomoglogyIso (f , eqs) n)) =
+  Iso.ret (fst (chainComplexEquiv→HomoglogyIso (f , eqs) n)) =
     funExt⁻ (cong fst (sym (chainComplexMap→HomologyMapComp f
                             (invChainMap (f , eqs)) n))
           ∙∙ cong (λ f → fst (chainComplexMap→HomologyMap f n))
@@ -323,10 +323,10 @@ homologyIso n C D chEq₂ chEq₁ chEq₀ eq1 eq2 = main-iso
       (PT.map (λ {(s , t)
       → (Iso.inv (chEq₂ .fst) s)
        , Σ≡Prop (λ _ → AbGroupStr.is-set (snd (chain C n)) _ _)
-           (sym (Iso.leftInv (chEq₁ .fst) _)
+           (sym (Iso.ret (chEq₁ .fst) _)
           ∙ cong (Iso.inv (chEq₁ .fst)) (funExt⁻ eq2 (Iso.inv (chEq₂ .fst) s))
           ∙ cong (Iso.inv (chEq₁ .fst) ∘ bdry D (suc n) .fst)
-                 (Iso.rightInv (chEq₂ .fst) s)
+                 (Iso.sec (chEq₂ .fst) s)
           ∙ cong (Iso.inv (chEq₁ .fst)) (cong fst t)
           ∙ IsGroupHom.pres· (invGroupIso chEq₁ .snd) _ _
           ∙ cong₂ (snd (chain C (suc n) ) .AbGroupStr._+_)
@@ -335,10 +335,10 @@ homologyIso n C D chEq₂ chEq₁ chEq₀ eq1 eq2 = main-iso
     where
     g : _ → homology n C .fst
     g (a , b) = [ Iso.inv (fst chEq₁) a
-                , sym (Iso.leftInv (chEq₀ .fst) _)
+                , sym (Iso.ret (chEq₀ .fst) _)
                 ∙ cong (Iso.inv (chEq₀ .fst)) (funExt⁻ eq1 (Iso.inv (chEq₁ .fst) a))
                 ∙ cong (Iso.inv (chEq₀ .fst) ∘ bdry D n  .fst)
-                       (Iso.rightInv (chEq₁ .fst) a)
+                       (Iso.sec (chEq₁ .fst) a)
                 ∙ cong (Iso.inv (chEq₀ .fst)) b
                 ∙ IsGroupHom.pres1 (invGroupIso chEq₀ .snd) ]
 
@@ -354,16 +354,16 @@ homologyIso n C D chEq₂ chEq₁ chEq₀ eq1 eq2 = main-iso
   main-iso : GroupIso (homology n C) (homology n D)
   Iso.fun (fst main-iso) = F
   Iso.inv (fst main-iso) = G
-  Iso.rightInv (fst main-iso) =
+  Iso.sec (fst main-iso) =
     elimProp (λ _ → GroupStr.is-set (homology n D .snd) _ _)
       λ{(a , b)
       → cong [_] (Σ≡Prop (λ _
         → AbGroupStr.is-set (snd (chain D n)) _ _)
-                  (Iso.rightInv (fst chEq₁) a))}
-  Iso.leftInv (fst main-iso) =
+                  (Iso.sec (fst chEq₁) a))}
+  Iso.ret (fst main-iso) =
     elimProp (λ _ → GroupStr.is-set (homology n C .snd) _ _)
       λ{(a , b)
       → cong [_] (Σ≡Prop (λ _
         → AbGroupStr.is-set (snd (chain C n)) _ _)
-                  (Iso.leftInv (fst chEq₁) a))}
+                  (Iso.ret (fst chEq₁) a))}
   snd main-iso = F-hom

Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/OnCoproduct.agda

@@ -98,7 +98,7 @@ module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) w
               ≡ Iso.inv isoR (CommAlgebra→CommRing (R [ I ⊎ J ]) , baseRingHom)
       step1 i = Iso.inv isoR ((CommAlgebra→CommRing R[I⊎J]overR[I]) , ≡RingHoms i)
 
-      step2 = Iso.leftInv isoR (R [ I ⊎ J ])
+      step2 = Iso.ret isoR (R [ I ⊎ J ])
 
   fst≡R[I⊎J] : cong fst ≡R[I⊎J] ≡ refl
   fst≡R[I⊎J] =

Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/Properties.agda

@@ -278,8 +278,8 @@ homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
              → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))
 Iso.fun (homMapIso A) = evaluateAt A
 Iso.inv (homMapIso A) = inducedHom A
-Iso.rightInv (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
-Iso.leftInv (homMapIso {R = R} {I = I} A) =
+Iso.sec (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
+Iso.ret (homMapIso {R = R} {I = I} A) =
   λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
                (Theory.homRetrievable A f)
 
@@ -344,7 +344,7 @@ module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
   natIndHomR ψ ϕ = isoFunInjective (homMapIso B) _ _
                 (evaluateAt B (ψ ∘a (inducedHom A ϕ))        ≡⟨ refl ⟩
                  fst ψ ∘ evaluateAt A (inducedHom A ϕ)       ≡⟨ refl ⟩
-                 fst ψ ∘ ϕ                                   ≡⟨ Iso.rightInv (homMapIso B) _ ⟩
+                 fst ψ ∘ ϕ                                   ≡⟨ Iso.sec (homMapIso B) _ ⟩
                  evaluateAt B (inducedHom B (fst ψ ∘ ϕ))     ∎)
 
   {-

Cubical/Algebra/CommAlgebra/AsModule/Instances/Initial.agda

@@ -117,12 +117,12 @@ module _ (R : CommRing ℓ) where
         asIso : Iso (fst A) (fst initialCAlg)
         Iso.fun asIso = fst to
         Iso.inv asIso = fst from
-        Iso.rightInv asIso =
+        Iso.sec asIso =
           λ x i → cong
                     fst
                     (isContr→isProp (initialityContr initialCAlg) (to ∘a from) (idCAlgHom initialCAlg))
                     i x
-        Iso.leftInv asIso =
+        Iso.ret asIso =
           λ x i → cong
                     fst
                     (isContr→isProp (isInitial A) (from ∘a to) (idCAlgHom A))

Cubical/Algebra/CommAlgebra/AsModule/Localisation.agda

@@ -211,8 +211,8 @@ module AlgLocTwoSubsets (R' : CommRing ℓ)
   IsoS₁⁻¹RS₂⁻¹R : Iso S₁⁻¹R S₂⁻¹R
   Iso.fun IsoS₁⁻¹RS₂⁻¹R = fst χ₁
   Iso.inv IsoS₁⁻¹RS₂⁻¹R = fst χ₂
-  Iso.rightInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₁∘χ₂≡id)
-  Iso.leftInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₂∘χ₁≡id)
+  Iso.sec IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₁∘χ₂≡id)
+  Iso.ret IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong fst χ₂∘χ₁≡id)
 
   isContrS₁⁻¹R≅S₂⁻¹R : isContr (CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg)
   isContrS₁⁻¹R≅S₂⁻¹R = center , uniqueness

Cubical/Algebra/CommAlgebra/AsModule/Properties.agda

@@ -139,8 +139,8 @@ module CommAlgChar (R : CommRing ℓ) {ℓ' : Level} where
  CommAlgIso : Iso (CommAlgebra R ℓ') CommRingWithHom
  fun CommAlgIso = fromCommAlg
  inv CommAlgIso = toCommAlg
- rightInv CommAlgIso = CommRingWithHomRoundTrip
- leftInv CommAlgIso = CommAlgRoundTrip
+ sec CommAlgIso = CommRingWithHomRoundTrip
+ ret CommAlgIso = CommAlgRoundTrip
 
  open IsCommRingHom
 
@@ -301,8 +301,8 @@ contrCommAlgebraHom→contrCommAlgebraEquiv σ contrHom x y = σEquiv ,
   σIso : Iso ⟨ σ x ⟩ ⟨ σ y ⟩
   fun σIso = fst χ₁
   inv σIso = fst χ₂
-  rightInv σIso = funExt⁻ (cong fst χ₁∘χ₂≡id)
-  leftInv σIso = funExt⁻ (cong fst χ₂∘χ₁≡id)
+  sec σIso = funExt⁻ (cong fst χ₁∘χ₂≡id)
+  ret σIso = funExt⁻ (cong fst χ₂∘χ₁≡id)
 
   σEquiv : CommAlgebraEquiv (σ x) (σ y)
   fst σEquiv = isoToEquiv σIso

Cubical/Algebra/CommAlgebra/Instances/Initial.agda

@@ -80,12 +80,12 @@ module _ (R : CommRing ℓ) where
         asIso : Iso ⟨ A ⟩ₐ ⟨ initialCAlg ⟩ₐ
         Iso.fun asIso = fst to
         Iso.inv asIso = fst from
-        Iso.rightInv asIso =
+        Iso.sec asIso =
           λ x i → cong
                     fst
                     (isContr→isProp (initialityContr initialCAlg) (to ∘ca from) (idCAlgHom initialCAlg))
                     i x
-        Iso.leftInv asIso =
+        Iso.ret asIso =
           λ x i → cong
                     fst
                     (isContr→isProp (isInitial A) (from ∘ca to) (idCAlgHom A))

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -204,8 +204,8 @@ module AlgLocTwoSubsets (R' : CommRing ℓ)
   IsoS₁⁻¹RS₂⁻¹R : Iso S₁⁻¹R S₂⁻¹R
   Iso.fun IsoS₁⁻¹RS₂⁻¹R = ⟨ χ₁ ⟩ₐ→
   Iso.inv IsoS₁⁻¹RS₂⁻¹R = ⟨ χ₂ ⟩ₐ→
-  Iso.rightInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong ⟨_⟩ₐ→ χ₁∘χ₂≡id)
-  Iso.leftInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong ⟨_⟩ₐ→ χ₂∘χ₁≡id)
+  Iso.sec IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong ⟨_⟩ₐ→ χ₁∘χ₂≡id)
+  Iso.ret IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong ⟨_⟩ₐ→ χ₂∘χ₁≡id)
 
   isContrS₁⁻¹R≅S₂⁻¹R : isContr (CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg)
   isContrS₁⁻¹R≅S₂⁻¹R = center , uniqueness

Cubical/Algebra/CommAlgebra/Polynomials.agda

@@ -59,8 +59,8 @@ homMapIso : {R : CommRing ℓ} {I : Type ℓ''} (A : CommAlgebra R ℓ')
              → Iso (CommAlgebraHom (R [ I ]) A) (I → (fst A))
 Iso.fun (homMapIso A) = evaluateAt A
 Iso.inv (homMapIso A) = inducedHom A
-Iso.rightInv (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
-Iso.leftInv (homMapIso {R = R} {I = I} A) =
+Iso.sec (homMapIso A) = λ ϕ → Theory.mapRetrievable A ϕ
+Iso.ret (homMapIso {R = R} {I = I} A) =
   λ f → Σ≡Prop (λ f → isPropIsCommAlgebraHom {M = R [ I ]} {N = A} f)
                (Theory.homRetrievable A f)
 
@@ -125,7 +125,7 @@ module _ {R : CommRing ℓ} {A B : CommAlgebra R ℓ''} where
   natIndHomR ψ ϕ = isoFunInjective (homMapIso B) _ _
                 (evaluateAt B (ψ ∘a (inducedHom A ϕ))        ≡⟨ refl ⟩
                  fst ψ ∘ evaluateAt A (inducedHom A ϕ)       ≡⟨ refl ⟩
-                 fst ψ ∘ ϕ                                   ≡⟨ Iso.rightInv (homMapIso B) _ ⟩
+                 fst ψ ∘ ϕ                                   ≡⟨ Iso.sec (homMapIso B) _ ⟩
                  evaluateAt B (inducedHom B (fst ψ ∘ ϕ))     ∎)
 
   {-

Cubical/Algebra/CommRing/Properties.agda

@@ -185,7 +185,7 @@ module _ where
 
   injCommRingIso : {R : CommRing ℓ} {S : CommRing ℓ'} (f : CommRingIso R S)
                  → (x y : R .fst) → f .fst .fun x ≡ f .fst .fun y → x ≡ y
-  injCommRingIso f x y h = sym (f .fst .leftInv x) ∙∙ cong (f .fst .inv) h ∙∙ f .fst .leftInv y
+  injCommRingIso f x y h = sym (f .fst .ret x) ∙∙ cong (f .fst .inv) h ∙∙ f .fst .ret y
 
 module _ where
   open RingEquivs
@@ -342,8 +342,8 @@ module CommRingUAFunctoriality where
                                                 , commringstr (q0 i) (q1 i) (r+ i) (r· i) (s i) (t i)
    inv theIso x = cong ⟨_⟩ x , cong (0r ∘ snd) x , cong (1r ∘ snd) x
                 , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (isCommRing ∘ snd) x
-   rightInv theIso _ = refl
-   leftInv theIso _ = refl
+   sec theIso _ = refl
+   ret theIso _ = refl
 
  caracCommRing≡ : {A B : CommRing ℓ} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
  caracCommRing≡ {A = A} {B = B} p q P =

Cubical/Algebra/CommRing/Univalence.agda

@@ -58,16 +58,16 @@ fst (fun (CommRingEquivIsoCommRingIso R S) e) = equivToIso (e .fst)
 snd (fun (CommRingEquivIsoCommRingIso R S) e) = e .snd
 fst (inv (CommRingEquivIsoCommRingIso R S) e) = isoToEquiv (e .fst)
 snd (inv (CommRingEquivIsoCommRingIso R S) e) = e .snd
-rightInv (CommRingEquivIsoCommRingIso R S) (e , he) =
+sec (CommRingEquivIsoCommRingIso R S) (e , he) =
   Σ≡Prop (λ e → isPropIsCommRingHom (snd R) (e .fun) (snd S))
          rem
   where
   rem : equivToIso (isoToEquiv e) ≡ e
   fun (rem i) x = fun e x
   inv (rem i) x = inv e x
-  rightInv (rem i) b j = CommRingStr.is-set (snd S) (fun e (inv e b)) b (rightInv e b) (rightInv e b) i j
-  leftInv (rem i) a j = CommRingStr.is-set (snd R) (inv e (fun e a)) a (retEq (isoToEquiv e) a) (leftInv e a) i j
-leftInv (CommRingEquivIsoCommRingIso R S) e =
+  sec (rem i) b j = CommRingStr.is-set (snd S) (fun e (inv e b)) b (sec e b) (sec e b) i j
+  ret (rem i) a j = CommRingStr.is-set (snd R) (inv e (fun e a)) a (retEq (isoToEquiv e) a) (ret e a) i j
+ret (CommRingEquivIsoCommRingIso R S) e =
   Σ≡Prop (λ e → isPropIsCommRingHom (snd R) (e .fst) (snd S))
          (equivEq refl)
 

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

@@ -416,6 +416,6 @@ module _
     is : Iso (⊕HIT ℕ G Gstr) (⊕Fun G Gstr)
     fun is = ⊕HIT→⊕Fun
     Iso.inv is = ⊕Fun→⊕HIT
-    rightInv is = e-sect
-    leftInv is = e-retr
+    sec is = e-sect
+    ret is = e-retr
   snd Equiv-DirectSum = makeIsGroupHom ⊕HIT→⊕Fun-pres+

Cubical/Algebra/GradedRing/Instances/TrivialGradedRing.agda

@@ -101,11 +101,11 @@ module _
       inv is = DS-Rec-Set.f _ _ _ _ is-set
                0r (λ {zero a → a ; (suc k) a → 0r }) _+_ +Assoc +IdR +Comm
                (λ { zero → refl ; (suc k) → refl}) (λ {zero a b → refl ; (suc n) a b → +IdR _})
-      rightInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
+      sec is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _)
                     (base-neutral _)
                     (λ { zero a → refl ; (suc k) a → base-neutral _ ∙ sym (base-neutral _)} )
                     λ {U V} ind-U ind-V → sym (base-add _ _ _) ∙ cong₂ _add_ ind-U ind-V
-      leftInv is = λ _ → refl
+      ret is = λ _ → refl
     snd equivRing = makeIsRingHom
                     -- issue agda have trouble infering the Idx, G, Gstr
                     {R = ARing}