diff --git a/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda b/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda index a72ba69860..f4b56f0e41 100644 --- a/Cubical/Algebra/AbGroup/Instances/FreeAbGroup.agda +++ b/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 diff --git a/Cubical/Algebra/AbGroup/Instances/IntMod.agda b/Cubical/Algebra/AbGroup/Instances/IntMod.agda index 553a3a2f1b..c03adb429d 100644 --- a/Cubical/Algebra/AbGroup/Instances/IntMod.agda +++ b/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 _ _) diff --git a/Cubical/Algebra/AbGroup/TensorProduct.agda b/Cubical/Algebra/AbGroup/TensorProduct.agda index c4a16b3a49..6ed18b481b 100644 --- a/Cubical/Algebra/AbGroup/TensorProduct.agda +++ b/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) diff --git a/Cubical/Algebra/Algebra/Properties.agda b/Cubical/Algebra/Algebra/Properties.agda index afffe58e41..d5cee5e119 100644 --- a/Cubical/Algebra/Algebra/Properties.agda +++ b/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 = diff --git a/Cubical/Algebra/ChainComplex/Homology.agda b/Cubical/Algebra/ChainComplex/Homology.agda index 40ec460b66..0118e364fd 100644 --- a/Cubical/Algebra/ChainComplex/Homology.agda +++ b/Cubical/Algebra/ChainComplex/Homology.agda @@ -136,7 +136,7 @@ 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)) @@ -144,7 +144,7 @@ module _ where → Σ≡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 diff --git a/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/OnCoproduct.agda b/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/OnCoproduct.agda index 9bf3284da6..43b1dec96b 100644 --- a/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/OnCoproduct.agda +++ b/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] = diff --git a/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/Properties.agda b/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/Properties.agda index 3d65252918..59beacc20a 100644 --- a/Cubical/Algebra/CommAlgebra/AsModule/FreeCommAlgebra/Properties.agda +++ b/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 ψ ∘ ϕ)) ∎) {- diff --git a/Cubical/Algebra/CommAlgebra/AsModule/Instances/Initial.agda b/Cubical/Algebra/CommAlgebra/AsModule/Instances/Initial.agda index faec0afea0..e6d592e908 100644 --- a/Cubical/Algebra/CommAlgebra/AsModule/Instances/Initial.agda +++ b/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)) diff --git a/Cubical/Algebra/CommAlgebra/AsModule/Localisation.agda b/Cubical/Algebra/CommAlgebra/AsModule/Localisation.agda index e03f20fc9d..f43795f8f1 100644 --- a/Cubical/Algebra/CommAlgebra/AsModule/Localisation.agda +++ b/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 diff --git a/Cubical/Algebra/CommAlgebra/AsModule/Properties.agda b/Cubical/Algebra/CommAlgebra/AsModule/Properties.agda index 0d5a3f0720..bc9332c4c6 100644 --- a/Cubical/Algebra/CommAlgebra/AsModule/Properties.agda +++ b/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 diff --git a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda b/Cubical/Algebra/CommAlgebra/Instances/Initial.agda index 65b7141d3b..6cedb63285 100644 --- a/Cubical/Algebra/CommAlgebra/Instances/Initial.agda +++ b/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)) diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda index b49b0f93dc..8d475a1181 100644 --- a/Cubical/Algebra/CommAlgebra/Localisation.agda +++ b/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 diff --git a/Cubical/Algebra/CommAlgebra/Polynomials.agda b/Cubical/Algebra/CommAlgebra/Polynomials.agda index 15f3b8398f..5ccb35047c 100644 --- a/Cubical/Algebra/CommAlgebra/Polynomials.agda +++ b/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 ψ ∘ ϕ)) ∎) {- diff --git a/Cubical/Algebra/CommRing/Properties.agda b/Cubical/Algebra/CommRing/Properties.agda index f8eaed91b0..e96539b4ca 100644 --- a/Cubical/Algebra/CommRing/Properties.agda +++ b/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 = diff --git a/Cubical/Algebra/CommRing/Univalence.agda b/Cubical/Algebra/CommRing/Univalence.agda index 39c86f2c40..70f0d0de1f 100644 --- a/Cubical/Algebra/CommRing/Univalence.agda +++ b/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) diff --git a/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda b/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda index 5b3f3c3351..a356768911 100644 --- a/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda +++ b/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+ diff --git a/Cubical/Algebra/GradedRing/Instances/TrivialGradedRing.agda b/Cubical/Algebra/GradedRing/Instances/TrivialGradedRing.agda index dfa052a335..a9a76662b7 100644 --- a/Cubical/Algebra/GradedRing/Instances/TrivialGradedRing.agda +++ b/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} diff --git a/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda b/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda index f07b624f32..0910e97b7d 100644 --- a/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda +++ b/Cubical/Algebra/Group/Abelianization/AbelianizationAsCoeq.agda @@ -367,7 +367,7 @@ module IsoCoeqHIT (G : Group ℓ) where where r : (x : fst asAbelianGroup) → fst (compGroupHom (GroupIso→GroupHom h) (GroupIso→GroupHom (invGroupIso h))) x ≡ x - r = λ x → (h .fst .Iso.leftInv) x + r = λ x → (h .fst .Iso.ret) x leftInvGroupHom : (compGroupHom (GroupIso→GroupHom h) diff --git a/Cubical/Algebra/Group/Abelianization/Properties.agda b/Cubical/Algebra/Group/Abelianization/Properties.agda index 75b7dcbef2..90106b993b 100644 --- a/Cubical/Algebra/Group/Abelianization/Properties.agda +++ b/Cubical/Algebra/Group/Abelianization/Properties.agda @@ -356,9 +356,9 @@ fst (AbelianizationEquiv {G = G} {H} ϕ) = isoToEquiv main main : Iso _ _ Iso.fun main = fst (AbelianizationFun (GroupEquiv→GroupHom ϕ)) Iso.inv main = fst (AbelianizationFun (GroupEquiv→GroupHom (invGroupEquiv ϕ))) - Iso.rightInv main = + Iso.sec main = elimProp _ (λ _ → isset _ _) λ g → cong η (secEq (fst ϕ) g) - Iso.leftInv main = + Iso.ret main = elimProp _ (λ _ → isset _ _) λ g → cong η (retEq (fst ϕ) g) snd (AbelianizationEquiv {G = G} {H} ϕ) = snd (AbelianizationFun (fst (fst ϕ) , snd ϕ)) @@ -370,8 +370,8 @@ Iso.inv (fst (AbelianizationIdempotent G)) = rec _ (AbGroupStr.is-set (snd G)) (λ x → x) λ a b c → cong (AbGroupStr._+_ (snd G) a) (AbGroupStr.+Comm (snd G) _ _) -Iso.rightInv (fst (AbelianizationIdempotent G)) = +Iso.sec (fst (AbelianizationIdempotent G)) = elimProp _ (λ _ → isset _ _) (λ _ → refl) -Iso.leftInv (fst (AbelianizationIdempotent G)) x = refl +Iso.ret (fst (AbelianizationIdempotent G)) x = refl snd (AbelianizationIdempotent G) = snd (AbelianizationGroupStructure.ηAsGroupHom _) diff --git a/Cubical/Algebra/Group/Five.agda b/Cubical/Algebra/Group/Five.agda index 2ae7a590d4..2c75c0c33e 100644 --- a/Cubical/Algebra/Group/Five.agda +++ b/Cubical/Algebra/Group/Five.agda @@ -142,7 +142,7 @@ module _ d = pInv d' p[d]≡t[c'] : p .fun .fst d ≡ t .fst c' - p[d]≡t[c'] = Iso.rightInv pIso d' + p[d]≡t[c'] = Iso.sec pIso d' u[p[d]] : ⟨ E' ⟩ u[p[d]] = u .fst (p .fun .fst d) @@ -227,7 +227,7 @@ module _ b = mInv b' m[b]≡b' : m .fun .fst b ≡ b' - m[b]≡b' = Iso.rightInv mIso b' + m[b]≡b' = Iso.sec mIso b' s[m[b]]≡s[b'] : s .fst (m .fun .fst b) ≡ s .fst b' s[m[b]]≡s[b'] = cong (s .fst) m[b]≡b' diff --git a/Cubical/Algebra/Group/Free.agda b/Cubical/Algebra/Group/Free.agda index 2540e9ecbf..a85ceffd69 100644 --- a/Cubical/Algebra/Group/Free.agda +++ b/Cubical/Algebra/Group/Free.agda @@ -425,11 +425,11 @@ module NormalForm (A : Type ℓ) where η·iso : (Bool × A) → Iso (Σ [𝟚× A ] IsNormalised) (Σ [𝟚× A ] IsNormalised) Iso.fun (η·iso x) = nη· x Iso.inv (η·iso x) = nη· (not₁ x) - Iso.rightInv (η·iso x) b = + Iso.sec (η·iso x) b = Σ≡Prop isPropIsNormalised (funExt⁻ (cong η· (sym (not₁not₁ x)) ) (η· (not₁ x) (fst b)) ∙ sec-preη· (not₁ x) _ (HeadIsRedex? _) (HeadIsRedex? _) (snd b)) - Iso.leftInv (η·iso x) a = + Iso.ret (η·iso x) a = Σ≡Prop isPropIsNormalised (sec-preη· x _ (HeadIsRedex? _) (HeadIsRedex? _) (snd a)) @@ -461,9 +461,9 @@ module NormalForm (A : Type ℓ) where ∘S ⇊1g++comm a' (invLi b') ∘S ≡ε ∘S flip (·⁻¹≡ε-trans _ _ _) (·⁻¹≡ε-sym _ _ t') ∘S ·⁻¹≡ε-trans _ _ _ t - rightInv IsoNF = SQ.elimProp (λ _ → squash/ _ _) + sec IsoNF = SQ.elimProp (λ _ → squash/ _ _) (eq/ _ _ ∘ fst ∘ snd ∘ normalise) - leftInv IsoNF = Σ≡Prop isPropIsNormalised ∘ uncurry + ret IsoNF = Σ≡Prop isPropIsNormalised ∘ uncurry (Li.elim (λ _ → refl) λ f v → let lem : ∀ uu → preη· _ _ uu ≡ _ ∷ _ lem = diff --git a/Cubical/Algebra/Group/Instances/Bool.agda b/Cubical/Algebra/Group/Instances/Bool.agda index b65e48f670..fcbece1914 100644 --- a/Cubical/Algebra/Group/Instances/Bool.agda +++ b/Cubical/Algebra/Group/Instances/Bool.agda @@ -66,15 +66,15 @@ module _ {ℓ : Level} {A : Group ℓ} (e : Iso (fst A) Bool) where true→1 : Iso.fun IsoABool true ≡ 1g (snd A) true→1 with (Iso.fun e (1g (snd A))) ≟ true - ... | yes p = sym (cong (Iso.inv e) p) ∙ Iso.leftInv e _ + ... | yes p = sym (cong (Iso.inv e) p) ∙ Iso.ret e _ ... | no p = sym (cong (Iso.inv e) (¬true→false (Iso.fun e (1g (snd A))) p)) - ∙ Iso.leftInv e (1g (snd A)) + ∙ Iso.ret e (1g (snd A)) decA : (x : typ A) → (x ≡ 1g (snd A)) ⊎ (x ≡ Iso.fun IsoABool false) decA x with (Iso.inv IsoABool x) ≟ false | discreteA x (1g (snd A)) ... | yes p | yes q = inl q - ... | yes p | no q = inr (sym (Iso.rightInv IsoABool x) ∙ cong (Iso.fun (IsoABool)) p) - ... | no p | no q = inr (⊥.rec (q (sym (Iso.rightInv IsoABool x) + ... | yes p | no q = inr (sym (Iso.sec IsoABool x) ∙ cong (Iso.fun (IsoABool)) p) + ... | no p | no q = inr (⊥.rec (q (sym (Iso.sec IsoABool x) ∙∙ cong (Iso.fun IsoABool) (¬false→true _ p) ∙∙ true→1))) ... | no p | yes q = inl q diff --git a/Cubical/Algebra/Group/Instances/IntMod.agda b/Cubical/Algebra/Group/Instances/IntMod.agda index cbc2dea0e8..ee570d7ed3 100644 --- a/Cubical/Algebra/Group/Instances/IntMod.agda +++ b/Cubical/Algebra/Group/Instances/IntMod.agda @@ -57,14 +57,14 @@ Iso.inv (fst Bool≅ℤGroup/2) (zero , p) = true Iso.inv (fst Bool≅ℤGroup/2) (suc zero , p) = false Iso.inv (fst Bool≅ℤGroup/2) (suc (suc x) , p) = ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p))) -Iso.rightInv (fst Bool≅ℤGroup/2) (zero , p) = +Iso.sec (fst Bool≅ℤGroup/2) (zero , p) = Σ≡Prop (λ _ → isProp≤) refl -Iso.rightInv (fst Bool≅ℤGroup/2) (suc zero , p) = +Iso.sec (fst Bool≅ℤGroup/2) (suc zero , p) = Σ≡Prop (λ _ → isProp≤) refl -Iso.rightInv (fst Bool≅ℤGroup/2) (suc (suc x) , p) = +Iso.sec (fst Bool≅ℤGroup/2) (suc (suc x) , p) = ⊥.rec (¬-<-zero (predℕ-≤-predℕ (predℕ-≤-predℕ p))) -Iso.leftInv (fst Bool≅ℤGroup/2) false = refl -Iso.leftInv (fst Bool≅ℤGroup/2) true = refl +Iso.ret (fst Bool≅ℤGroup/2) false = refl +Iso.ret (fst Bool≅ℤGroup/2) true = refl snd Bool≅ℤGroup/2 = makeIsGroupHom λ { false false → refl ; false true → refl diff --git a/Cubical/Algebra/Group/Instances/Pi.agda b/Cubical/Algebra/Group/Instances/Pi.agda index 8c592a0463..5d149f7523 100644 --- a/Cubical/Algebra/Group/Instances/Pi.agda +++ b/Cubical/Algebra/Group/Instances/Pi.agda @@ -47,6 +47,6 @@ snd (ΠGroupHom fam) = Iso.fun (fst (ΠGroupIso fam)) = fst (ΠGroupHom λ a → GroupIso→GroupHom (fam a)) Iso.inv (fst (ΠGroupIso fam)) = fst (ΠGroupHom λ a → GroupIso→GroupHom (invGroupIso (fam a))) -Iso.rightInv (fst (ΠGroupIso fam)) f = funExt λ x → Iso.rightInv (fst (fam x)) _ -Iso.leftInv (fst (ΠGroupIso fam)) f = funExt λ x → Iso.leftInv (fst (fam x)) _ +Iso.sec (fst (ΠGroupIso fam)) f = funExt λ x → Iso.sec (fst (fam x)) _ +Iso.ret (fst (ΠGroupIso fam)) f = funExt λ x → Iso.ret (fst (fam x)) _ snd (ΠGroupIso fam) = snd (ΠGroupHom λ a → GroupIso→GroupHom (fam a)) diff --git a/Cubical/Algebra/Group/Instances/Unit.agda b/Cubical/Algebra/Group/Instances/Unit.agda index 54fb8ac437..90107e4d56 100644 --- a/Cubical/Algebra/Group/Instances/Unit.agda +++ b/Cubical/Algebra/Group/Instances/Unit.agda @@ -46,15 +46,15 @@ open Iso lUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd UnitGroup₀ G) G fun (fst lUnitGroupIso) = snd inv (fst lUnitGroupIso) g = tt , g -rightInv (fst lUnitGroupIso) _ = refl -leftInv (fst lUnitGroupIso) _ = refl +sec (fst lUnitGroupIso) _ = refl +ret (fst lUnitGroupIso) _ = refl snd lUnitGroupIso = makeIsGroupHom λ _ _ → refl rUnitGroupIso : {G : Group ℓ} → GroupIso (DirProd G UnitGroup₀) G fun (fst rUnitGroupIso) = fst inv (fst rUnitGroupIso) g = g , tt -rightInv (fst rUnitGroupIso) _ = refl -leftInv (fst rUnitGroupIso) _ = refl +sec (fst rUnitGroupIso) _ = refl +ret (fst rUnitGroupIso) _ = refl snd rUnitGroupIso = makeIsGroupHom λ _ _ → refl -- lifted version @@ -62,16 +62,16 @@ lUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'} → GroupIso (DirProd (UnitGroup {ℓ}) G) G fun (fst lUnitGroupIso^) = snd inv (fst lUnitGroupIso^) = tt* ,_ -rightInv (fst lUnitGroupIso^) g = refl -leftInv (fst lUnitGroupIso^) (tt* , g) = refl +sec (fst lUnitGroupIso^) g = refl +ret (fst lUnitGroupIso^) (tt* , g) = refl snd lUnitGroupIso^ = makeIsGroupHom λ _ _ → refl rUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'} → GroupIso (DirProd G (UnitGroup {ℓ})) G fun (fst rUnitGroupIso^) = fst inv (fst rUnitGroupIso^) = _, tt* -rightInv (fst rUnitGroupIso^) g = refl -leftInv (fst rUnitGroupIso^) (g , tt*) = refl +sec (fst rUnitGroupIso^) g = refl +ret (fst rUnitGroupIso^) (g , tt*) = refl snd rUnitGroupIso^ = makeIsGroupHom λ _ _ → refl lUnitGroupEquiv : {G : Group ℓ} → GroupEquiv (DirProd UnitGroup₀ G) G @@ -83,8 +83,8 @@ rUnitGroupEquiv = GroupIso→GroupEquiv rUnitGroupIso contrGroupIsoUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupIso G UnitGroup₀ fun (fst (contrGroupIsoUnit contr)) _ = tt inv (fst (contrGroupIsoUnit contr)) _ = fst contr -rightInv (fst (contrGroupIsoUnit contr)) _ = refl -leftInv (fst (contrGroupIsoUnit contr)) x = snd contr x +sec (fst (contrGroupIsoUnit contr)) _ = refl +ret (fst (contrGroupIsoUnit contr)) x = snd contr x snd (contrGroupIsoUnit contr) = makeIsGroupHom λ _ _ → refl contrGroupEquivUnit : {G : Group ℓ} → isContr ⟨ G ⟩ → GroupEquiv G UnitGroup₀ diff --git a/Cubical/Algebra/Group/IsomorphismTheorems.agda b/Cubical/Algebra/Group/IsomorphismTheorems.agda index 1f5bb7278d..e81577b019 100644 --- a/Cubical/Algebra/Group/IsomorphismTheorems.agda +++ b/Cubical/Algebra/Group/IsomorphismTheorems.agda @@ -98,8 +98,8 @@ module _ {G H : Group ℓ} (ϕ : GroupHom G H) where isoThm1 : GroupIso imϕ (G / kerNormalSubgroup) fun (fst isoThm1) = f1 inv (fst isoThm1) = f2 - rightInv (fst isoThm1) = f12 - leftInv (fst isoThm1) = f21 + sec (fst isoThm1) = f12 + ret (fst isoThm1) = f21 snd isoThm1 = makeIsGroupHom f1-isHom -- The SIP lets us turn the isomorphism theorem into a path diff --git a/Cubical/Algebra/Group/MorphismProperties.agda b/Cubical/Algebra/Group/MorphismProperties.agda index 937e1398c1..5513fcd153 100644 --- a/Cubical/Algebra/Group/MorphismProperties.agda +++ b/Cubical/Algebra/Group/MorphismProperties.agda @@ -257,10 +257,10 @@ fun (fst (GroupIsoDirProd iso1 iso2)) prod = fun (fst iso1) (fst prod) , fun (fst iso2) (snd prod) inv (fst (GroupIsoDirProd iso1 iso2)) prod = inv (fst iso1) (fst prod) , inv (fst iso2) (snd prod) -rightInv (fst (GroupIsoDirProd iso1 iso2)) a = - ΣPathP (rightInv (fst iso1) (fst a) , (rightInv (fst iso2) (snd a))) -leftInv (fst (GroupIsoDirProd iso1 iso2)) a = - ΣPathP (leftInv (fst iso1) (fst a) , (leftInv (fst iso2) (snd a))) +sec (fst (GroupIsoDirProd iso1 iso2)) a = + ΣPathP (sec (fst iso1) (fst a) , (sec (fst iso2) (snd a))) +ret (fst (GroupIsoDirProd iso1 iso2)) a = + ΣPathP (ret (fst iso1) (fst a) , (ret (fst iso2) (snd a))) snd (GroupIsoDirProd iso1 iso2) = makeIsGroupHom λ a b → ΣPathP (pres· (snd iso1) (fst a) (fst b) , pres· (snd iso2) (snd a) (snd b)) @@ -302,8 +302,8 @@ BijectionIso→GroupIso {G = G} {H = H} i = grIso grIso : GroupIso G H fun (fst grIso) = f inv (fst grIso) b = rec (helper b) (λ a → a) (surj i b) .fst - rightInv (fst grIso) b = rec (helper b) (λ a → a) (surj i b) .snd - leftInv (fst grIso) b j = rec (helper (f b)) (λ a → a) + sec (fst grIso) b = rec (helper b) (λ a → a) (surj i b) .snd + ret (fst grIso) b j = rec (helper (f b)) (λ a → a) (isPropPropTrunc (surj i (f b)) ∣ b , refl ∣₁ j) .fst snd grIso = snd (fun i) diff --git a/Cubical/Algebra/Group/Properties.agda b/Cubical/Algebra/Group/Properties.agda index c2cb2a51f8..771f3fc636 100644 --- a/Cubical/Algebra/Group/Properties.agda +++ b/Cubical/Algebra/Group/Properties.agda @@ -106,11 +106,11 @@ congIdLeft≡congIdRight _·G_ -G_ 0G rUnitG lUnitG r≡l p = ·GroupAutomorphismL : ∀ {ℓ} (G : Group ℓ) (g : fst G) → Iso (fst G) (fst G) Iso.fun (·GroupAutomorphismL G g) = GroupStr._·_ (snd G) g Iso.inv (·GroupAutomorphismL G g) = GroupStr._·_ (snd G) (GroupStr.inv (snd G) g) -Iso.rightInv (·GroupAutomorphismL G g) h = +Iso.sec (·GroupAutomorphismL G g) h = GroupStr.·Assoc (snd G) _ _ _ ∙ cong₂ (GroupStr._·_ (snd G)) (GroupStr.·InvR (snd G) g) refl ∙ GroupStr.·IdL (snd G) h -Iso.leftInv (·GroupAutomorphismL G g) h = +Iso.ret (·GroupAutomorphismL G g) h = GroupStr.·Assoc (snd G) _ _ _ ∙ cong₂ (GroupStr._·_ (snd G)) (GroupStr.·InvL (snd G) g) refl ∙ GroupStr.·IdL (snd G) h @@ -118,11 +118,11 @@ Iso.leftInv (·GroupAutomorphismL G g) h = ·GroupAutomorphismR : ∀ {ℓ} (G : Group ℓ) (g : fst G) → Iso (fst G) (fst G) Iso.fun (·GroupAutomorphismR G g) x = GroupStr._·_ (snd G) x g Iso.inv (·GroupAutomorphismR G g) x = GroupStr._·_ (snd G) x (GroupStr.inv (snd G) g) -Iso.rightInv (·GroupAutomorphismR G g) h = +Iso.sec (·GroupAutomorphismR G g) h = sym (GroupStr.·Assoc (snd G) _ _ _) ∙ cong₂ (GroupStr._·_ (snd G)) refl (GroupStr.·InvL (snd G) g) -- ∙ GroupStr.·IdR (snd G) h -Iso.leftInv (·GroupAutomorphismR G g) h = +Iso.ret (·GroupAutomorphismR G g) h = sym (GroupStr.·Assoc (snd G) _ _ _) ∙ cong₂ (GroupStr._·_ (snd G)) refl (GroupStr.·InvR (snd G) g) -- ∙ GroupStr.·IdR (snd G) h diff --git a/Cubical/Algebra/Group/QuotientGroup.agda b/Cubical/Algebra/Group/QuotientGroup.agda index 5a1c9d9061..4b4fe1f5df 100644 --- a/Cubical/Algebra/Group/QuotientGroup.agda +++ b/Cubical/Algebra/Group/QuotientGroup.agda @@ -139,9 +139,9 @@ module _ {G' : Group ℓ} (H' : NormalSubgroup G') Iso.fun (fst trivialRelIso) g = [ g ] Iso.inv (fst trivialRelIso) = rec is-set (λ g → g) contrH - Iso.rightInv (fst trivialRelIso) = + Iso.sec (fst trivialRelIso) = elimProp (λ _ → squash/ _ _) λ _ → refl - Iso.leftInv (fst trivialRelIso) _ = refl + Iso.ret (fst trivialRelIso) _ = refl snd trivialRelIso = makeIsGroupHom λ _ _ → refl @@ -169,10 +169,10 @@ Iso.fun (fst (Hom/Iso {G' = G'} {H' = H'} ϕ ϕ' ψ')) = fst (Hom/ {G' = G'} {H' = H'} (GroupIso→GroupHom ϕ) ϕ') Iso.inv (fst (Hom/Iso {G' = G'} {H' = H'} ϕ ϕ' ψ')) = fst (Hom/ {G' = H'} {H' = G'} (GroupIso→GroupHom (invGroupIso ϕ)) ψ') -Iso.rightInv (fst (Hom/Iso ϕ ϕ' ψ')) = - elimProp (λ _ → squash/ _ _) λ a → cong [_] (Iso.rightInv (fst ϕ) a) -Iso.leftInv (fst (Hom/Iso ϕ ϕ' ψ')) = - elimProp (λ _ → squash/ _ _) λ a → cong [_] (Iso.leftInv (fst ϕ) a) +Iso.sec (fst (Hom/Iso ϕ ϕ' ψ')) = + elimProp (λ _ → squash/ _ _) λ a → cong [_] (Iso.sec (fst ϕ) a) +Iso.ret (fst (Hom/Iso ϕ ϕ' ψ')) = + elimProp (λ _ → squash/ _ _) λ a → cong [_] (Iso.ret (fst ϕ) a) snd (Hom/Iso {G' = G'} {H' = H'} ϕ ϕ' ψ') = makeIsGroupHom λ x y → IsGroupHom.pres· (snd (Hom/ {G' = G'} {H' = H'} @@ -206,6 +206,6 @@ Hom/ImIso {G = G} {H} ϕ {G'} {H'} ψ {ϕ'} {ψ'} eG eH e∼ = ∙ sym (IsGroupHom.pres· (snd (invGroupIso eH)) a (GroupStr.inv (H' .snd) b)) ∙ cong (Iso.inv (fst eH)) (sym p) - ∙ cong (Iso.inv (fst eH) ∘ fst ψ) (sym (Iso.rightInv (fst eG) x))) + ∙ cong (Iso.inv (fst eH) ∘ fst ψ) (sym (Iso.sec (fst eG) x))) ∙ cong (Iso.inv (fst eH)) (e∼ (Iso.inv (fst eG) x)) - ∙ Iso.leftInv (fst eH) _))) + ∙ Iso.ret (fst eH) _))) diff --git a/Cubical/Algebra/Group/ZAction.agda b/Cubical/Algebra/Group/ZAction.agda index 79d069cb75..64ffad0981 100644 --- a/Cubical/Algebra/Group/ZAction.agda +++ b/Cubical/Algebra/Group/ZAction.agda @@ -204,7 +204,7 @@ Iso-pres-gen₁ : ∀ {ℓ ℓ'} (G : Group ℓ) (H : Group ℓ') (g : fst G) → gen₁-by H (fun (fst e) g) Iso-pres-gen₁ G H g genG is h = (fst (genG (inv (fst is) h))) - , (sym (rightInv (fst is) h) + , (sym (sec (fst is) h) ∙∙ cong (fun (fst is)) (snd (genG (inv (fst is) h))) ∙∙ (homPresℤ· (_ , snd is) g (fst (genG (inv (fst is) h))))) @@ -213,7 +213,7 @@ Iso-pres-gen₂ : (G : Group ℓ) (H : Group ℓ') (g₁ g₂ : fst G) → gen₂-by H (fun (fst e) g₁) (fun (fst e) g₂) fst (Iso-pres-gen₂ G H g₁ g₂ genG is h) = genG (inv (fst is) h) .fst snd (Iso-pres-gen₂ G H g₁ g₂ genG is h) = - sym (rightInv (fst is) h) + sym (sec (fst is) h) ∙∙ cong (fun (fst is)) (snd (genG (inv (fst is) h))) ∙∙ (pres· (snd is) _ _ ∙ cong₂ (_·_ (snd H)) diff --git a/Cubical/Algebra/Matrix.agda b/Cubical/Algebra/Matrix.agda index 9ad955160c..bfe2fde235 100644 --- a/Cubical/Algebra/Matrix.agda +++ b/Cubical/Algebra/Matrix.agda @@ -70,8 +70,8 @@ VecMatrix→FinMatrix→VecMatrix {m = suc m} (M ∷ MS) i = FinMatrixIsoVecMatrix : (A : Type ℓ) (m n : ℕ) → Iso (FinMatrix A m n) (VecMatrix A m n) fun (FinMatrixIsoVecMatrix A m n) = FinMatrix→VecMatrix inv (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix -rightInv (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix→VecMatrix -leftInv (FinMatrixIsoVecMatrix A m n) = FinMatrix→VecMatrix→FinMatrix +sec (FinMatrixIsoVecMatrix A m n) = VecMatrix→FinMatrix→VecMatrix +ret (FinMatrixIsoVecMatrix A m n) = FinMatrix→VecMatrix→FinMatrix FinMatrix≃VecMatrix : {m n : ℕ} → FinMatrix A m n ≃ VecMatrix A m n FinMatrix≃VecMatrix {_} {A} {m} {n} = isoToEquiv (FinMatrixIsoVecMatrix A m n) diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/AB-An[X]Bn[X].agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/AB-An[X]Bn[X].agda index 22835e5ebb..1ce68f1e93 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/AB-An[X]Bn[X].agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/AB-An[X]Bn[X].agda @@ -84,11 +84,11 @@ module _ is : Iso (fst PA) (fst PB) fun is = fst (makeCommRingHomPoly A' B' n (f , fstr)) inv is = fst (makeCommRingHomPoly B' A' n (g , gstr)) - rightInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) + sec is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) refl (λ v a → cong (base v) (secEq e a)) λ {U V} ind-U ind-V → cong₂ (_+_ (snd PB)) ind-U ind-V - leftInv is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) + ret is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) refl (λ v a → cong (base v) (retEq e a)) λ {U V} ind-U ind-V → cong₂ (_+_ (snd PA)) ind-U ind-V diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda index 08d51550b3..ebfc124a91 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/A[X]X-A.agda @@ -241,8 +241,8 @@ module _ is : Iso (A[x1,···,xn]/ Ar 1 0 1) A fun is = A[x]/x→A inv is = A→A[x]/x - rightInv is = e-sect - leftInv is = e-retr + sec is = e-sect + ret is = e-retr snd Equiv-A[X]/X-A = snd A[X]/X→A Equiv-ℤ[X]/X-ℤ : RingEquiv (CommRing→Ring ℤ[X]/X) (CommRing→Ring ℤCR) diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[Am[X]]-Anm[X].agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[Am[X]]-Anm[X].agda index dd36453369..2c2870e428 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[Am[X]]-Anm[X].agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[Am[X]]-Anm[X].agda @@ -140,7 +140,7 @@ module _ (A' : CommRing ℓ) (n m : ℕ) where is : Iso _ _ Iso.fun is = PAmn→PAn+m Iso.inv is = PAn+m→PAmn - Iso.rightInv is = e-sect - Iso.leftInv is = e-retr + Iso.sec is = e-sect + Iso.ret is = e-retr snd CRE-PolyN∘M-PolyN+M = makeIsCommRingHom PAmn→PAn+m-pres1 PAmn→PAn+m-pres+ PAmn→PAn+m-pres· diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda index ce90949db1..d6fbc5acb7 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/An[X]X-A.agda @@ -267,8 +267,8 @@ module _ is : Iso (A[x1,···,xn]/ Ar n) A fun is = PAI→A inv is = A→PAI - rightInv is = e-sect - leftInv is = e-retr + sec is = e-sect + ret is = e-retr snd Equiv-QuotientX-A = snd PAIr→Ar -- Warning this doesn't prove Z[X]/X ≅ ℤ because you get two definition, diff --git a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/Poly0-A.agda b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/Poly0-A.agda index cda6f67824..d5ef378bf2 100644 --- a/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/Poly0-A.agda +++ b/Cubical/Algebra/Polynomials/Multivariate/EquivCarac/Poly0-A.agda @@ -86,6 +86,6 @@ module _ (A' : CommRing ℓ) where is : Iso (Poly A' 0) (A' .fst) Iso.fun is = Poly0→A Iso.inv is = A→Poly0 - Iso.rightInv is = e-sect - Iso.leftInv is = e-retr + Iso.sec is = e-sect + Iso.ret is = e-retr snd CRE-Poly0-A = makeIsCommRingHom Poly0→A-pres1 Poly0→A-pres+ Poly0→A-pres· diff --git a/Cubical/Algebra/Polynomials/TypevariateHIT/EquivUnivariateListPoly.agda b/Cubical/Algebra/Polynomials/TypevariateHIT/EquivUnivariateListPoly.agda index aeb66b08e5..cf9faeaf45 100644 --- a/Cubical/Algebra/Polynomials/TypevariateHIT/EquivUnivariateListPoly.agda +++ b/Cubical/Algebra/Polynomials/TypevariateHIT/EquivUnivariateListPoly.agda @@ -65,8 +65,8 @@ module _ {R : CommRing ℓ} where typevariateListPolyIso : Iso ⟨ R [ Unit ] ⟩ ⟨ ListPolyCommAlgebra R ⟩ fun typevariateListPolyIso = fst to inv typevariateListPolyIso = fst from - rightInv typevariateListPolyIso = toFrom - leftInv typevariateListPolyIso = fromTo + sec typevariateListPolyIso = toFrom + ret typevariateListPolyIso = fromTo typevariateListPolyEquiv : CommAlgebraEquiv (R [ Unit ]) (ListPolyCommAlgebra R) fst typevariateListPolyEquiv = isoToEquiv typevariateListPolyIso diff --git a/Cubical/Algebra/Polynomials/UnivariateList/Poly1-1Poly.agda b/Cubical/Algebra/Polynomials/UnivariateList/Poly1-1Poly.agda index e074b964db..222137e335 100644 --- a/Cubical/Algebra/Polynomials/UnivariateList/Poly1-1Poly.agda +++ b/Cubical/Algebra/Polynomials/UnivariateList/Poly1-1Poly.agda @@ -172,8 +172,8 @@ module _ (Acr : CommRing ℓ) where is : Iso _ _ Iso.fun is = Poly1→Poly: Iso.inv is = Poly:→Poly1 - Iso.rightInv is = e-sect - Iso.leftInv is = e-retr + Iso.sec is = e-sect + Iso.ret is = e-retr snd CRE-Poly1-Poly: = makeIsCommRingHom Poly1→Poly:-pres1 Poly1→Poly:-pres+ diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda index d3a07111c9..ab5255856f 100644 --- a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda @@ -218,8 +218,8 @@ module AdjBij {ℓ : Level} where → Iso (CommRingHom A (𝓞 .F-ob X)) (X ⇒ Sp .F-ob A) fun 𝓞⊣SpIso = _♭ inv 𝓞⊣SpIso = _♯ - rightInv 𝓞⊣SpIso = ♭♯Id - leftInv 𝓞⊣SpIso = ♯♭Id + sec 𝓞⊣SpIso = ♭♯Id + ret 𝓞⊣SpIso = ♯♭Id 𝓞⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) → (β ●ᵛ α) ♯ ≡ (𝓞 .F-hom β) ∘cr (α ♯) @@ -241,9 +241,9 @@ module AdjBij {ℓ : Level} where theIso : Iso (A .fst) ((𝓞 ∘F Sp) .F-ob A .fst) fun theIso = ε A .fst inv theIso = yonedaᴾ 𝔸¹ A .fun - rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α - leftInv theIso a = path -- I get yellow otherwise + sec theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .ret α + ret theIso a = path -- I get yellow otherwise where path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a - path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a + path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .sec a snd (𝓞⊣SpCounitEquiv A) = ε A .snd diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda index 23475be058..b37635757c 100644 --- a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/CompactOpen.agda @@ -360,7 +360,7 @@ module _ {ℓ : Level} where U .N-ob R[1/ (f i) ]AsCommRing (X .F-hom /1AsCommRingHom x) ≡⟨ cong (U .N-ob R[1/ f i ]AsCommRing) - (funExt⁻ (cong fst (isoX .rightInv (compatibleFamIncl fam))) i) ⟩ + (funExt⁻ (cong fst (isoX .sec (compatibleFamIncl fam))) i) ⟩ U .N-ob R[1/ (f i) ]AsCommRing (fam .fst i .fst) @@ -372,11 +372,11 @@ module _ {ℓ : Level} where inducedZarLatHom /1AsCommRingHom .fst (D R 1r) ∎ - rightInv isoU fam = + sec isoU fam = Σ≡Prop (λ _ → isPropIsCompatibleFamily _ _ _) (funExt λ i → Σ≡Prop (λ _ → squash/ _ _) (funExt⁻ (cong fst - (isoX .rightInv (compatibleFamIncl fam))) i)) - leftInv isoU y = Σ≡Prop (λ _ → squash/ _ _) + (isoX .sec (compatibleFamIncl fam))) i)) + ret isoU y = Σ≡Prop (λ _ → squash/ _ _) (cong (isoX .inv) (compatibleFamIncl≡ y) - ∙ isoX .leftInv (y .fst)) + ∙ isoX .ret (y .fst)) diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda index 17a019016f..3b9479c345 100644 --- a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda +++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/OpenSubscheme.agda @@ -184,7 +184,7 @@ module _ {ℓ : Level} (R : CommRing ℓ) (W : CompactOpen (Sp ⟅ R ⟆)) where ⋁Df≡W : ⋁ (CompOpenDistLattice ⟅ Sp ⟅ R ⟆ ⟆) (D R ∘ f) ≡ W ⋁Df≡W = sym (pres⋁ (_ , isHomYoneda) (ZL.D R ∘ f)) ∙ cong (yonedaᴾ ZarLatFun R .inv) ⋁Df≡w - ∙ yonedaᴾ ZarLatFun R .leftInv W + ∙ yonedaᴾ ZarLatFun R .ret W makeAffineCoverCompOpenOfAffine : AffineCover ⟦ W ⟧ᶜᵒ makeAffineCoverCompOpenOfAffine = toAffineCover f ⋁Df≡W diff --git a/Cubical/Axiom/Omniscience.agda b/Cubical/Axiom/Omniscience.agda index dae8793718..1924579156 100644 --- a/Cubical/Axiom/Omniscience.agda +++ b/Cubical/Axiom/Omniscience.agda @@ -75,8 +75,8 @@ module WLPO≃ where total≡points P = isoToPath λ where .fun → points P .inv → total P - .rightInv never → isPropΠ (λ x → isProp¬ ⟨ P x ⟩) _ never - .leftInv α≡f → isSet→ isSetBool P (const false) _ α≡f + .sec never → isPropΠ (λ x → isProp¬ ⟨ P x ⟩) _ never + .ret α≡f → isSet→ isSetBool P (const false) _ α≡f WLPO≡WLPO' : WLPO A ≡ WLPO' A WLPO≡WLPO' {A = A} i = (P : A → 𝟚) → Dec (WLPO≃.total≡points P (~ i)) diff --git a/Cubical/CW/Approximation.agda b/Cubical/CW/Approximation.agda index c4b819a35e..e2d88acfbe 100644 --- a/Cubical/CW/Approximation.agda +++ b/Cubical/CW/Approximation.agda @@ -280,7 +280,7 @@ finCWmap→CellMap n C D f = PT.map (λ {(ϕ , p) → ψ ϕ (funExt⁻ p) , funExt λ x → subst (λ x → realiseCellMap (ψ ϕ (funExt⁻ p)) x ≡ f x) - (Iso.rightInv (converges→ColimIso + (Iso.sec (converges→ColimIso {seq = realiseSeq (finCWskel→CWskel n C)} n (C .snd .snd)) x) (cong (incl {n = n}) (silly ϕ (funExt⁻ p) _) diff --git a/Cubical/CW/ChainComplex.agda b/Cubical/CW/ChainComplex.agda index 7f8cd8b518..7fdc820734 100644 --- a/Cubical/CW/ChainComplex.agda +++ b/Cubical/CW/ChainComplex.agda @@ -148,12 +148,12 @@ module _ {ℓ} (C : CWskel ℓ) where iso-cancel-1 : suspFun (isoCofBouquetInv↑ n) ∘ suspFun (isoCofBouquet (suc n)) ≡ λ x → x iso-cancel-1 = sym (suspFunComp _ _) - ∙∙ cong suspFun (λ i x → Iso.leftInv + ∙∙ cong suspFun (λ i x → Iso.ret (BouquetIso-gen (suc n) (An+1 n) (αn+1 n) (snd C .snd .snd .snd (suc n))) x i) ∙∙ suspFunIdFun iso-cancel-2 : (isoSuspBouquetInv↑ n) ∘ (isoSuspBouquet (suc n)) ≡ λ x → x - iso-cancel-2 i x = Iso.leftInv sphereBouquetSuspIso x i + iso-cancel-2 i x = Iso.ret sphereBouquetSuspIso x i left-maps = (isoSuspBouquet↑ n) ∘ (suspFun (isoSuspBouquet n)) ∘ (suspFun (suspFun (isoCofBouquet n))) ∘ (suspFun (suspFun (to_cofibCW n C))) @@ -232,7 +232,7 @@ module _ {ℓ} (C : CWskel ℓ) where opaque preϵpre∂≡0 : ∀ (x : SphereBouquet 1 (Fin (preboundary.An+1 0))) → (preϵ ∘ preboundary.pre∂ 0) x ≡ inl tt preϵpre∂≡0 x = cong (ε ∘ (suspFun isoCofBouquetInv)) - (Iso.leftInv sphereBouquetSuspIso + (Iso.ret sphereBouquetSuspIso (((suspFun isoCofBouquet) ∘ (suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x)) ∙ cong ε (aux (((suspFun (to_cofibCW 0 C)) ∘ (δ 1 C) ∘ isoCofBouquetInv↑) x)) ∙ εδ (isoCofBouquetInv↑ x) @@ -241,7 +241,7 @@ module _ {ℓ} (C : CWskel ℓ) where aux : ∀ (x : Susp (cofibCW 0 C)) → (suspFun (isoCofBouquetInv) ∘ (suspFun isoCofBouquet)) x ≡ x aux north = refl aux south = refl - aux (merid a i) j = merid (Iso.leftInv (BouquetIso-gen 0 An αn (snd C .snd .snd .snd 0)) a j) i + aux (merid a i) j = merid (Iso.ret (BouquetIso-gen 0 An αn (snd C .snd .snd .snd 0)) a j) i ϵ : AbGroupHom (ℤ[A 0 ]) (ℤ[Fin 1 ]) ϵ = bouquetDegree preϵ diff --git a/Cubical/CW/Connected.agda b/Cubical/CW/Connected.agda index c85d2c85fb..2864cd5bc1 100644 --- a/Cubical/CW/Connected.agda +++ b/Cubical/CW/Connected.agda @@ -364,8 +364,8 @@ module shrinkPushoutLemma (A : Type ℓ) (B : Type ℓ') Iso-PushoutF-Pushout-g∘f : Iso (Pushout F fst) (Pushout (g ∘ f) fst) Iso.fun Iso-PushoutF-Pushout-g∘f = PushoutF→Pushout-g∘f Iso.inv Iso-PushoutF-Pushout-g∘f = Pushout-g∘f-fst→Unit⊎A - Iso.rightInv Iso-PushoutF-Pushout-g∘f = PushoutF→Pushout-g∘f→PushoutF - Iso.leftInv Iso-PushoutF-Pushout-g∘f = Pushout-g∘f→PushoutF→Pushout-g∘f + Iso.sec Iso-PushoutF-Pushout-g∘f = PushoutF→Pushout-g∘f→PushoutF + Iso.ret Iso-PushoutF-Pushout-g∘f = Pushout-g∘f→PushoutF→Pushout-g∘f module CWLemmas-0Connected where @@ -400,8 +400,8 @@ module CWLemmas-0Connected where ≡ f (Unit⊎Fin→Fin y , x) help (inl a) false = sym p help (inl b) true = Σ≡Prop (λ _ → isProp<ᵗ) refl - help (inr a) false = Iso.leftInv Iso-Fin-Unit⊎Fin _ - help (inr a) true = Iso.leftInv Iso-Fin-Unit⊎Fin _ + help (inr a) false = Iso.ret Iso-Fin-Unit⊎Fin _ + help (inr a) true = Iso.ret Iso-Fin-Unit⊎Fin _ -- If the domain of f is instead Fin 1 × S⁰, this must also be the -- codomain of f. @@ -442,8 +442,8 @@ module CWLemmas-0Connected where mainIso : Iso (Fin 1 × S₊ 0) (Fin (suc (suc m))) Iso.fun mainIso = f Iso.inv mainIso x = isSurj-α₀ (suc zero) m f c x .fst - Iso.rightInv mainIso x = isSurj-α₀ 1 m f c x .snd - Iso.leftInv mainIso ((zero , tt) , x) = + Iso.sec mainIso x = isSurj-α₀ 1 m f c x .snd + Iso.ret mainIso ((zero , tt) , x) = (f-inj _ _ (isSurj-α₀ 1 m f c (f (fzero , x)) .snd)) -- Strengthening of shrinkImageAttachingMapLem for domain of f of @@ -506,9 +506,9 @@ module CWLemmas-0Connected where ¬f'≡flast : ¬ (f' (flast , true) ≡ flast) ¬f'≡flast p = xpath (cong f (ΣPathP (sym (swapFinβₗ flast x₀) , refl)) - ∙ sym (Iso.rightInv FinIso2 _) + ∙ sym (Iso.sec FinIso2 _) ∙ cong (Iso.inv FinIso2) (p ∙ sym f'≡flast) - ∙ Iso.rightInv FinIso2 _ + ∙ Iso.sec FinIso2 _ ∙ cong f (ΣPathP (swapFinβₗ flast x₀ , refl))) f'-bound : fst (f' (flast , true)) <ᵗ suc m @@ -522,7 +522,7 @@ module CWLemmas-0Connected where (isoToEquiv FinIso2) (isoToEquiv (swapFinIso flast x₀)) (funExt (λ x → cong (FinIso2 .Iso.fun ∘ f) - (sym (Iso.rightInv Fin×S⁰-swapIso x)))) + (sym (Iso.sec Fin×S⁰-swapIso x)))) refl -- the main lemma: a pushout of f : Fin n × S⁰ → Fin m is equivalent diff --git a/Cubical/CW/Homology/Base.agda b/Cubical/CW/Homology/Base.agda index e2ee70456f..84c9689a8e 100644 --- a/Cubical/CW/Homology/Base.agda +++ b/Cubical/CW/Homology/Base.agda @@ -117,11 +117,11 @@ H̃ˢᵏᵉˡ→Iso : {C : CWskel ℓ} {D : CWskel ℓ'} (m : ℕ) (e : realise C ≃ realise D) → GroupIso (H̃ˢᵏᵉˡ C m) (H̃ˢᵏᵉˡ D m) Iso.fun (fst (H̃ˢᵏᵉˡ→Iso m e)) = fst (H̃ˢᵏᵉˡ→ m (fst e)) Iso.inv (fst (H̃ˢᵏᵉˡ→Iso m e)) = fst (H̃ˢᵏᵉˡ→ m (invEq e)) -Iso.rightInv (fst (H̃ˢᵏᵉˡ→Iso m e)) = +Iso.sec (fst (H̃ˢᵏᵉˡ→Iso m e)) = funExt⁻ (cong fst (sym (H̃ˢᵏᵉˡ→comp m (fst e) (invEq e)) ∙∙ cong (H̃ˢᵏᵉˡ→ m) (funExt (secEq e)) ∙∙ H̃ˢᵏᵉˡ→id m)) -Iso.leftInv (fst (H̃ˢᵏᵉˡ→Iso m e)) = +Iso.ret (fst (H̃ˢᵏᵉˡ→Iso m e)) = funExt⁻ (cong fst (sym (H̃ˢᵏᵉˡ→comp m (invEq e) (fst e)) ∙∙ cong (H̃ˢᵏᵉˡ→ m) (funExt (retEq e)) ∙∙ H̃ˢᵏᵉˡ→id m)) @@ -233,11 +233,11 @@ H̃ᶜʷ→Iso : {C : CW ℓ} {D : CW ℓ'} (m : ℕ) (e : fst C ≃ fst D) → GroupIso (H̃ᶜʷ C m) (H̃ᶜʷ D m) Iso.fun (fst (H̃ᶜʷ→Iso m e)) = fst (H̃ᶜʷ→ m (fst e)) Iso.inv (fst (H̃ᶜʷ→Iso m e)) = fst (H̃ᶜʷ→ m (invEq e)) -Iso.rightInv (fst (H̃ᶜʷ→Iso m e)) = +Iso.sec (fst (H̃ᶜʷ→Iso m e)) = funExt⁻ (cong fst (sym (H̃ᶜʷ→comp m (fst e) (invEq e)) ∙∙ cong (H̃ᶜʷ→ m) (funExt (secEq e)) ∙∙ H̃ᶜʷ→id m)) -Iso.leftInv (fst (H̃ᶜʷ→Iso m e)) = +Iso.ret (fst (H̃ᶜʷ→Iso m e)) = funExt⁻ (cong fst (sym (H̃ᶜʷ→comp m (invEq e) (fst e)) ∙∙ cong (H̃ᶜʷ→ m) (funExt (retEq e)) ∙∙ H̃ᶜʷ→id m)) diff --git a/Cubical/CW/Homology/Groups/CofibFinSphereBouquetMap.agda b/Cubical/CW/Homology/Groups/CofibFinSphereBouquetMap.agda index 8f2420a317..8b7263d494 100644 --- a/Cubical/CW/Homology/Groups/CofibFinSphereBouquetMap.agda +++ b/Cubical/CW/Homology/Groups/CofibFinSphereBouquetMap.agda @@ -84,19 +84,19 @@ module _ {c1 c2 : ℕ} {n : ℕ} (α : FinSphereBouquetMap c1 c2 n) where HₙSphereBouquetⁿ/→ℤ[]/ImSphereMap-fun p q inv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre p q) = HₙSphereBouquetⁿ/→ℤ[]/ImSphereMap-inv p q - rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (lt x) q) f = + sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (lt x) q) f = ⊥.rec (¬m<ᵗm x) - rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (lt y)) f = refl - rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (eq y)) f = refl - rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (gt y)) f = refl - rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (gt x) q) f = + sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (lt y)) f = refl + sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (eq y)) f = refl + sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (gt y)) f = refl + sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (gt x) q) f = ⊥.rec (¬m<ᵗm x) - leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (lt x) q) f = + ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (lt x) q) f = ⊥.rec (¬m<ᵗm x) - leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (lt y)) f = refl - leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (eq y)) f = refl - leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (gt y)) f = refl - leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (gt x) q) f = + ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (lt y)) f = refl + ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (eq y)) f = refl + ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (eq x) (gt y)) f = refl + ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (gt x) q) f = ⊥.rec (¬m<ᵗm x) HₙSphereBouquetⁿ/→ℤ[]/ImSphereMap-fun-hom : @@ -311,14 +311,14 @@ module _ {c1 c2 : ℕ} {n : ℕ} (α : FinSphereBouquetMap c1 c2 n) where HₙSphereBouquetⁿ/→ℤ[]/ImSphereMap inv (fst GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap) = ℤ[]/ImSphereMap→HₙSphereBouquetⁿ/ - rightInv (fst GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap) = + sec (fst GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap) = SQ.elimProp (λ _ → squash/ _ _) - λ f → cong [_] (rightInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre + λ f → cong [_] (sec (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (suc n ≟ᵗ suc n) (suc n ≟ᵗ suc (suc n))) f) - leftInv (fst GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap) = + ret (fst GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap) = SQ.elimProp (λ _ → squash/ _ _) λ f → cong [_] (Σ≡Prop (λ _ → isSetΠ (λ _ → isSetℤ) _ _) - (leftInv (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre + (ret (Iso-HₙSphereBouquetⁿ/-ℤ[]/ImSphereMap-pre (suc n ≟ᵗ suc n) (suc n ≟ᵗ suc (suc n))) (fst f))) snd GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap = makeIsGroupHom HₙSphereBouquetⁿ/→ℤ[]/ImSphereMap-hom diff --git a/Cubical/CW/Homology/Groups/Sn.agda b/Cubical/CW/Homology/Groups/Sn.agda index 4f4ec9f954..cab3631d00 100644 --- a/Cubical/CW/Homology/Groups/Sn.agda +++ b/Cubical/CW/Homology/Groups/Sn.agda @@ -80,8 +80,8 @@ module _ (n : ℕ) where ℤ≅HₙSⁿ : GroupIso ℤGroup (H̃ˢᵏᵉˡ (Sˢᵏᵉˡ (suc n)) (suc n)) fun (fst ℤ≅HₙSⁿ) = ℤ→HₙSⁿ .fst inv (fst ℤ≅HₙSⁿ) = HₙSⁿ→ℤ - rightInv (fst ℤ≅HₙSⁿ) = HₙSⁿ→ℤ→HₙSⁿ - leftInv (fst ℤ≅HₙSⁿ) _ = refl + sec (fst ℤ≅HₙSⁿ) = HₙSⁿ→ℤ→HₙSⁿ + ret (fst ℤ≅HₙSⁿ) _ = refl snd ℤ≅HₙSⁿ = ℤ→HₙSⁿ .snd HₙSⁿ≅ℤ : GroupIso (H̃ˢᵏᵉˡ (Sˢᵏᵉˡ (suc n)) (suc n)) ℤGroup diff --git a/Cubical/CW/Homology/Groups/Subcomplex.agda b/Cubical/CW/Homology/Groups/Subcomplex.agda index 6f575c55f2..d0edef3c71 100644 --- a/Cubical/CW/Homology/Groups/Subcomplex.agda +++ b/Cubical/CW/Homology/Groups/Subcomplex.agda @@ -166,7 +166,7 @@ subComplexHomologyEquiv≡ C m n q = (funExt⁻ (CW↑GenComm C k (suc m) m (suc m ≟ᵗ suc k) q) x ∙ funExt⁻ (subComplex→map'Charac C m (suc m ≟ᵗ m) (m ≟ᵗ m)) (CW↑Gen (subComplex C m) k (suc m) (suc m ≟ᵗ suc k) q x) - ∙ cong (CW↪ C m) (sym (Iso.leftInv ( (realiseSubComplex m C) ) _) + ∙ cong (CW↪ C m) (sym (Iso.ret ( (realiseSubComplex m C) ) _) ∙ cong (Iso.inv (realiseSubComplex m C)) ((push _ ∙ cong (incl {n = suc m}) (cong (CW↪ (subComplex C m) m) diff --git a/Cubical/CW/Homotopy.agda b/Cubical/CW/Homotopy.agda index 0a5cd7ebf1..6eab04b67d 100644 --- a/Cubical/CW/Homotopy.agda +++ b/Cubical/CW/Homotopy.agda @@ -695,7 +695,7 @@ module chainHomEquation (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') ∘ suspFun (to_cofibCW (fst n) D) ∘ δ (suc (fst n)) D ∘ X ∘ Hn+1/Hn n ∘ Iso.inv (cofibIso (fst n) C)) - (sym (funExt (Iso.leftInv (BouquetIso D (suc (fst n)))))) + (sym (funExt (Iso.ret (BouquetIso D (suc (fst n)))))) -- connecting MMΣf to fn+1 bouquetΣf : bouquetDegree (bouquetMMmap merid-f merid-tt MMΣf) ≡ fn @@ -797,7 +797,7 @@ module chainHomEquationSuc (m : ℕ) (C : CWskel ℓ) (D : CWskel ℓ') ∘ (Hn+1/Hn (injectSuc n)) ∘ X ∘ suspFun (to_cofibCW (fst n) C) ∘ δ (suc (fst n)) C ∘ Iso.inv (BouquetIso C (suc (fst n)))) - (sym (funExt (Iso.leftInv (cofibIso (fst n) C)))) + (sym (funExt (Iso.ret (cofibIso (fst n) C)))) chainHomotopySuc : subtrGroupHom _ _ fn gn ≡ addGroupHom _ _ ∂H H∂' chainHomotopySuc = chainHomotopy2 ∙ cong (addGroupHom _ _ ∂H) bouquetΣH∂ diff --git a/Cubical/CW/HurewiczTheorem.agda b/Cubical/CW/HurewiczTheorem.agda index 031468afa5..952ab9904e 100644 --- a/Cubical/CW/HurewiczTheorem.agda +++ b/Cubical/CW/HurewiczTheorem.agda @@ -599,9 +599,9 @@ private λ k → cong (fst ϕ) (sym (cong (inv' (fst (π'ᵃᵇCofibFinSphereBouquetMap≅ℤ[]/BouquetDegree α))) (π'ᵃᵇCofibFinSphereBouquetMap≅ℤ[]/BouquetDegreePresGens α k)) - ∙ leftInv (fst (π'ᵃᵇCofibFinSphereBouquetMap≅ℤ[]/BouquetDegree α)) _) + ∙ ret (fst (π'ᵃᵇCofibFinSphereBouquetMap≅ℤ[]/BouquetDegree α)) _) ∙ hyp k - ∙ sym (leftInv (fst (GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap (fst α))) + ∙ sym (ret (fst (GroupIso-Hₙ₊₁SphereBouquetⁿ/→ℤ[]/ImSphereMap (fst α))) (genH̃ˢᵏᵉˡSphereBouquet/ˢᵏᵉˡ (fst α) k)) ∙ cong (ℤ[]/ImSphereMap→HₙSphereBouquetⁿ/ (fst α)) (isGen-genH̃ˢᵏᵉˡSphereBouquet/ˢᵏᵉˡ (fst α) k) @@ -1131,7 +1131,7 @@ private Xˢᵘᵇ→∙X₃₊ₙ : Xˢᵘᵇ∙ →∙ (X₃₊ₙ , CWskel∙ Xˢᵏᵉˡ (fst t) (suc (suc n))) fst Xˢᵘᵇ→∙X₃₊ₙ = inv' X₃₊ₙ≅X∞ - snd Xˢᵘᵇ→∙X₃₊ₙ = leftInv X₃₊ₙ≅X∞ _ + snd Xˢᵘᵇ→∙X₃₊ₙ = ret X₃₊ₙ≅X∞ _ Xˢᵘᵇ→∙X : Xˢᵘᵇ∙ →∙ X∙ Xˢᵘᵇ→∙X = (e∞⃖ , e∞⃖-incl) diff --git a/Cubical/CW/Instances/Pushout.agda b/Cubical/CW/Instances/Pushout.agda index 0a0005680b..6b8721e24f 100644 --- a/Cubical/CW/Instances/Pushout.agda +++ b/Cubical/CW/Instances/Pushout.agda @@ -191,12 +191,12 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ) → pushoutIso₀-inv (pushoutIso₀-fun x) ≡ x pushoutIso₀-leftInv (inl x) = (λ i → pushoutIso₀-helper - (Iso.leftInv (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) + (Iso.ret (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) (inl (CW₁-discrete C .fst x)) i)) ∙ λ i → inl (retEq (CW₁-discrete C) x i) pushoutIso₀-leftInv (inr x) = (λ i → pushoutIso₀-helper - (Iso.leftInv (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) + (Iso.ret (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) (inr (CW₁-discrete D .fst x)) i)) ∙ λ i → inr (retEq (CW₁-discrete D) x i) pushoutIso₀-leftInv (push a i) with (B .snd .snd .snd .fst a) @@ -219,7 +219,7 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ) pushoutIso₀-rightInv (inr x) = pushoutIso₀-helper₁ (Iso.inv (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) x) - ∙ λ i → inr (Iso.rightInv (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) x i) + ∙ λ i → inr (Iso.sec (Iso-Fin⊎Fin-Fin+ {card C zero} {card D zero}) x i) pushoutIso₀ : Iso (pushoutA (suc zero)) (Pushout pushoutMap₀ fst) pushoutIso₀ = @@ -322,8 +322,8 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ) IsoModifiedPushout : (n : ℕ) → Iso (pushoutA (suc (suc n))) (modifiedPushout n) Iso.fun (IsoModifiedPushout n) = Pushout→modifiedPushout n Iso.inv (IsoModifiedPushout n) = modifiedPushout→Pushout n - Iso.rightInv (IsoModifiedPushout n) = modP→Pushout→modP n - Iso.leftInv (IsoModifiedPushout n) = Pushout→modP→Pushout n + Iso.sec (IsoModifiedPushout n) = modP→Pushout→modP n + Iso.ret (IsoModifiedPushout n) = Pushout→modP→Pushout n pushoutIsoₛ-filler0 : (n : ℕ) (b : A B n) (x : S⁻ n) → I → I → pushoutA (suc n) pushoutIsoₛ-filler0 n b x i j = @@ -544,8 +544,8 @@ module CWPushout (ℓ : Level) (Bʷ Cʷ Dʷ : CWskel ℓ) pushoutIsoₛ : (n : ℕ) → Iso (modifiedPushout n) (Pushout (pushoutMapₛ n) fst) Iso.fun (pushoutIsoₛ n) = pushoutIsoₛ-fun n Iso.inv (pushoutIsoₛ n) = pushoutIsoₛ-inv n - Iso.rightInv (pushoutIsoₛ n) = pushoutIsoₛ-rightInv n - Iso.leftInv (pushoutIsoₛ n) = pushoutIsoₛ-leftInv n + Iso.sec (pushoutIsoₛ n) = pushoutIsoₛ-rightInv n + Iso.ret (pushoutIsoₛ n) = pushoutIsoₛ-leftInv n pushoutIsoₜ : (n : ℕ) → Iso (pushoutA (suc n)) (Pushout (pushoutMap n) fst) pushoutIsoₜ zero = pushoutIso₀ diff --git a/Cubical/CW/Instances/Sn.agda b/Cubical/CW/Instances/Sn.agda index 77dc9a0093..a936102ea3 100644 --- a/Cubical/CW/Instances/Sn.agda +++ b/Cubical/CW/Instances/Sn.agda @@ -138,10 +138,10 @@ fun (isPushoutSuspSphereIso n m e s) (merid a i) = push (fzero , a) i inv (isPushoutSuspSphereIso n m e s) (inl x) = north inv (isPushoutSuspSphereIso n m e s) (inr x) = south inv (isPushoutSuspSphereIso n m e s) (push a i) = merid (snd a) i -rightInv (isPushoutSuspSphereIso n m e s) (inl x) i = +sec (isPushoutSuspSphereIso n m e s) (inl x) i = inl (isContrSfamGen (suc n) m (subst (_<ᵗ suc n) e <ᵗsucm) s .snd x i) -rightInv (isPushoutSuspSphereIso n m e s) (inr (zero , tt)) j = inr fzero -rightInv (isPushoutSuspSphereIso n m e s) (push ((zero , tt) , a) i) = help i +sec (isPushoutSuspSphereIso n m e s) (inr (zero , tt)) j = inr fzero +sec (isPushoutSuspSphereIso n m e s) (push ((zero , tt) , a) i) = help i where ee = subst (_<ᵗ suc n) e <ᵗsucm help : Square {A = Pushout {A = Fin 1 × S₊ m} @@ -155,9 +155,9 @@ rightInv (isPushoutSuspSphereIso n m e s) (push ((zero , tt) , a) i) = help i (isContrSfamGen (suc n) m ee s .snd (Sgen.Sfam∙ (suc n) m s)) refl i j)) ◁ λ i j → push (fzero , a) i -leftInv (isPushoutSuspSphereIso n m e s) north = refl -leftInv (isPushoutSuspSphereIso n m e s) south = refl -leftInv (isPushoutSuspSphereIso n m e s) (merid a i) = refl +ret (isPushoutSuspSphereIso n m e s) north = refl +ret (isPushoutSuspSphereIso n m e s) south = refl +ret (isPushoutSuspSphereIso n m e s) (merid a i) = refl SfamGenTopElement : (n m : ℕ) → (n <ᵗ m) → (q : _) → S₊ n ≃ Sgen.Sfam n m q SfamGenTopElement n (suc m) p (lt x) = ⊥.rec (¬squeeze (x , p)) @@ -175,18 +175,18 @@ SuspSphere→Sphere (suc n) (merid a i) = merid a i IsoSucSphereSusp' : (n : ℕ) → Iso (S₊ (suc n)) (Susp (S₊ n)) fun (IsoSucSphereSusp' n) = fun (IsoSucSphereSusp n) inv (IsoSucSphereSusp' n) = SuspSphere→Sphere n -rightInv (IsoSucSphereSusp' zero) north = refl -rightInv (IsoSucSphereSusp' zero) south = SuspBool→S¹→SuspBool south -rightInv (IsoSucSphereSusp' zero) (merid a i) = +sec (IsoSucSphereSusp' zero) north = refl +sec (IsoSucSphereSusp' zero) south = SuspBool→S¹→SuspBool south +sec (IsoSucSphereSusp' zero) (merid a i) = SuspBool→S¹→SuspBool (merid a i) -rightInv (IsoSucSphereSusp' (suc n)) north = refl -rightInv (IsoSucSphereSusp' (suc n)) south = refl -rightInv (IsoSucSphereSusp' (suc n)) (merid a i) = refl -leftInv (IsoSucSphereSusp' zero) base = S¹→SuspBool→S¹ base -leftInv (IsoSucSphereSusp' zero) (loop i) = S¹→SuspBool→S¹ (loop i) -leftInv (IsoSucSphereSusp' (suc n)) north = refl -leftInv (IsoSucSphereSusp' (suc n)) south = refl -leftInv (IsoSucSphereSusp' (suc n)) (merid a i) = refl +sec (IsoSucSphereSusp' (suc n)) north = refl +sec (IsoSucSphereSusp' (suc n)) south = refl +sec (IsoSucSphereSusp' (suc n)) (merid a i) = refl +ret (IsoSucSphereSusp' zero) base = S¹→SuspBool→S¹ base +ret (IsoSucSphereSusp' zero) (loop i) = S¹→SuspBool→S¹ (loop i) +ret (IsoSucSphereSusp' (suc n)) north = refl +ret (IsoSucSphereSusp' (suc n)) south = refl +ret (IsoSucSphereSusp' (suc n)) (merid a i) = refl -- Our family Sfam satisfies the pushout property (i.e. is a CW complex) SαEqGen : (n m : ℕ) (p : Trichotomyᵗ (suc m) (suc n)) (q : _) diff --git a/Cubical/CW/Map.agda b/Cubical/CW/Map.agda index 6ed6d6663f..2cc6798750 100644 --- a/Cubical/CW/Map.agda +++ b/Cubical/CW/Map.agda @@ -137,7 +137,7 @@ module _ (m : ℕ) (C : CWskel ℓ) (n' : Fin m) where ∘ f ∘ Iso.inv (BouquetIso-gen n (card C n) (α C n) (e C n))) fn+1/fn-id - ∙ funExt (Iso.rightInv (BouquetIso-gen n (card C n) (α C n) (e C n))) + ∙ funExt (Iso.sec (BouquetIso-gen n (card C n) (α C n) (e C n))) chainFunct-id : chainFunct ≡ idGroupHom chainFunct-id = cong bouquetDegree bouquetFunct-id ∙ bouquetDegreeId @@ -170,7 +170,7 @@ module _ (m : ℕ) (g : finCellMap m D E) (f : finCellMap m C D) (n' : Fin m) wh bouquetFunct-comp = funExt λ x → cong (Iso.fun (BouquetIso-gen n (card E n) (α E n) (e E n))) (cong pf2.fn+1/fn - (Iso.leftInv (BouquetIso-gen n (card D n) (α D n) (e D n)) _) + (Iso.ret (BouquetIso-gen n (card D n) (α D n) (e D n)) _) ∙ funExt⁻ fn+1/fn-comp (Iso.inv (BouquetIso-gen n (card C n) (α C n) (e C n)) x)) @@ -253,11 +253,11 @@ module functoriality (m : ℕ) (f : finCellMap (suc m) C D) where → suspFun (inv (iso2 C (fst n))) (suspFun (fun (iso2 C (fst n))) x) ≡ x step3aux north = refl step3aux south = refl - step3aux (merid a i) j = merid (leftInv (iso2 C (fst n)) a j) i + step3aux (merid a i) j = merid (ret (iso2 C (fst n)) a j) i module _ (x : bouquet C (suc (fst n)) (suc (fst n))) where step1 = cong (suspFun (bouquetFunct (injectSuc n))) - (leftInv (iso1 C (fst n)) + (ret (iso1 C (fst n)) (((suspFun (fun (iso2 C (fst n)))) ∘ (suspFun (to_cofibCW (fst n) C)) ∘ (δ (suc (fst n)) C) ∘ (inv (iso2 C (suc (fst n))))) x)) @@ -292,7 +292,7 @@ module functoriality (m : ℕ) (f : finCellMap (suc m) C D) where step7 = cong ((suspFun (fun (iso2 D (fst n)))) ∘ (suspFun (to_cofibCW (fst n) D)) ∘ (δ (suc (fst n)) D)) - (sym (leftInv (iso2 D (suc (fst n))) + (sym (ret (iso2 D (suc (fst n))) (((fn+1/fn (fsuc n)) ∘ (inv (iso2 C (suc (fst n))))) x))) main = step1 ∙ step2 ∙ step3 ∙ step4 ∙ step5 ∙ step6 ∙ step7 @@ -341,7 +341,7 @@ module augmentationFunct (m : ℕ) (f : finCellMap (suc m) C D) where commPreϵ : (x : SphereBouquet 1 (A C 0)) → ((augmentation.preϵ D) ∘ (bouquetSusp→ (bouquetFunct fzero))) x ≡ augmentation.preϵ C x - commPreϵ x = cong ((ε D) ∘ (suspFun (inv (iso2 D)))) (leftInv (iso1 D) (((suspFun (bouquetFunct fzero)) ∘ (inv (iso1 C))) x)) + commPreϵ x = cong ((ε D) ∘ (suspFun (inv (iso2 D)))) (ret (iso1 D) (((suspFun (bouquetFunct fzero)) ∘ (inv (iso1 C))) x)) ∙ cong (ε D) (funExt⁻ aux (inv (iso1 C) x)) ∙ commε (((suspFun (inv (iso2 C))) ∘ (inv (iso1 C))) x) where @@ -360,7 +360,7 @@ module augmentationFunct (m : ℕ) (f : finCellMap (suc m) C D) where aux : (suspFun (inv (iso2 D))) ∘ (suspFun (bouquetFunct fzero)) ≡ (suspFun (fn+1/fn fzero)) ∘ (suspFun (inv (iso2 C))) aux = (sym (suspFunComp (inv (iso2 D)) (bouquetFunct fzero))) - ∙ cong suspFun (funExt (λ x → leftInv (iso2 D) (((fn+1/fn fzero) ∘ (inv (iso2 C))) x))) + ∙ cong suspFun (funExt (λ x → ret (iso2 D) (((fn+1/fn fzero) ∘ (inv (iso2 C))) x))) ∙ (suspFunComp (fn+1/fn fzero) (inv (iso2 C))) commϵFunct : compGroupHom (chainFunct fzero) (augmentation.ϵ D) diff --git a/Cubical/CW/Properties.agda b/Cubical/CW/Properties.agda index 66d531ffa9..c9bd5e41cb 100644 --- a/Cubical/CW/Properties.agda +++ b/Cubical/CW/Properties.agda @@ -63,9 +63,9 @@ CW₁-discrete C = compEquiv (snd C .snd .snd .snd 0) (isoToEquiv main) Iso.fun main (inl x) = ⊥.rec (CW₀-empty C x) Iso.fun main (inr x) = x Iso.inv main = inr - Iso.rightInv main x = refl - Iso.leftInv main (inl x) = ⊥.rec (CW₀-empty C x) - Iso.leftInv main (inr x) = refl + Iso.sec main x = refl + Iso.ret main (inl x) = ⊥.rec (CW₀-empty C x) + Iso.ret main (inr x) = refl -- elimination from Cₙ into prop CWskel→Prop : (C : CWskel ℓ) {A : (n : ℕ) → fst C n → Type ℓ'} @@ -205,7 +205,7 @@ satAC-CW₁ n C A = (λ _ → isOfHLevelPath (suc n) (isOfHLevelΠ (suc n) (λ _ → isOfHLevelTrunc (suc n))) _ _) λ f → funExt λ a → cong ∣_∣ - (funExt⁻ ((Iso.leftInv (domIsoDep (equivToIso fin→))) f) a)) + (funExt⁻ ((Iso.ret (domIsoDep (equivToIso fin→))) f) a)) satAC∃Fin-C0 : (C : CWskel ℓ) → satAC∃ ℓ' ℓ'' (fst C 1) satAC∃Fin-C0 C = diff --git a/Cubical/CW/Subcomplex.agda b/Cubical/CW/Subcomplex.agda index 92ee821bab..fd199131b6 100644 --- a/Cubical/CW/Subcomplex.agda +++ b/Cubical/CW/Subcomplex.agda @@ -153,8 +153,8 @@ module subComplexMapGen {ℓ : Level} (C : CWskel ℓ) where → Iso (fst C n) (SubComplexGen.subComplexFam C m n p) Iso.fun (subComplexIso m n ineq p) = subComplex←map' m n ineq p Iso.inv (subComplexIso m n ineq p) = subComplex→map' m n p - Iso.rightInv (subComplexIso m n ineq p) = retr-sect m n ineq p .fst - Iso.leftInv (subComplexIso m n ineq p) = retr-sect m n ineq p .snd + Iso.sec (subComplexIso m n ineq p) = retr-sect m n ineq p .fst + Iso.ret (subComplexIso m n ineq p) = retr-sect m n ineq p .snd subComplex→map : ∀ {ℓ} (C : CWskel ℓ) (m n : ℕ) → SubComplexGen.subComplexFam C m n (n ≟ᵗ m) → fst C n diff --git a/Cubical/Categories/Adjoint.agda b/Cubical/Categories/Adjoint.agda index 7d2b75dd8f..0e93bc54ad 100644 --- a/Cubical/Categories/Adjoint.agda +++ b/Cubical/Categories/Adjoint.agda @@ -88,8 +88,8 @@ module _ {F : Functor C D} {G : Functor D C} where Iso⊣^opF : Iso (F ⊣ G) ((G ^opF) ⊣ (F ^opF)) fun Iso⊣^opF = opositeAdjunction inv Iso⊣^opF = _ - rightInv Iso⊣^opF _ = refl - leftInv Iso⊣^opF _ = refl + sec Iso⊣^opF _ = refl + ret Iso⊣^opF _ = refl private variable @@ -207,22 +207,22 @@ module NaturalBijection where → g ♯ ⋆⟨ D ⟩ k ≡ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ adjNatInD' {c} {d} {d'} g k = g ♯ ⋆⟨ D ⟩ k - ≡⟨ sym (adjIso .leftInv (g ♯ ⋆⟨ D ⟩ k)) ⟩ + ≡⟨ sym (adjIso .ret (g ♯ ⋆⟨ D ⟩ k)) ⟩ ((g ♯ ⋆⟨ D ⟩ k) ♭) ♯ ≡⟨ cong _♯ (adjNatInD (g ♯) k) ⟩ ((g ♯) ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ - ≡⟨ cong _♯ (cong (λ g' → seq' C g' (G ⟪ k ⟫)) (adjIso .rightInv g)) ⟩ + ≡⟨ cong _♯ (cong (λ g' → seq' C g' (G ⟪ k ⟫)) (adjIso .sec g)) ⟩ (g ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ ∎ adjNatInC' : ∀ {c' c d} (f : D [ F ⟅ c ⟆ , d ]) (h : C [ c' , c ]) → h ⋆⟨ C ⟩ (f ♭) ≡ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭ adjNatInC' {c'} {c} {d} f h = h ⋆⟨ C ⟩ (f ♭) - ≡⟨ sym (adjIso .rightInv (h ⋆⟨ C ⟩ (f ♭))) ⟩ + ≡⟨ sym (adjIso .sec (h ⋆⟨ C ⟩ (f ♭))) ⟩ ((h ⋆⟨ C ⟩ (f ♭)) ♯) ♭ ≡⟨ cong _♭ (adjNatInC (f ♭) h) ⟩ ((F ⟪ h ⟫ ⋆⟨ D ⟩ (f ♭) ♯) ♭) - ≡⟨ cong _♭ (cong (λ f' → seq' D (F ⟪ h ⟫) f') (adjIso .leftInv f)) ⟩ + ≡⟨ cong _♭ (cong (λ f' → seq' D (F ⟪ h ⟫) f') (adjIso .ret f)) ⟩ (F ⟪ h ⟫ ⋆⟨ D ⟩ f) ♭ ∎ isLeftAdjoint : {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) → Type (ℓ-max (ℓ-max ℓC ℓC') (ℓ-max ℓD ℓD')) @@ -282,12 +282,12 @@ module _ (F : Functor C D) (G : Functor D C) where (F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) ♭ ≡⟨ sym (cong _♭ (adjNatInC _ _)) ⟩ (h ⋆⟨ C ⟩ g) ♯ ♭ - ≡⟨ adjIso .rightInv _ ⟩ + ≡⟨ adjIso .sec _ ⟩ h ⋆⟨ C ⟩ g ∎ C→D : (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫ ≡ h ⋆⟨ C ⟩ g) → (f ⋆⟨ D ⟩ k ≡ F ⟪ h ⟫ ⋆⟨ D ⟩ g ♯) C→D eq = f ⋆⟨ D ⟩ k - ≡⟨ sym (adjIso .leftInv _) ⟩ + ≡⟨ sym (adjIso .ret _) ⟩ (f ⋆⟨ D ⟩ k) ♭ ♯ ≡⟨ cong _♯ (adjNatInD _ _) ⟩ (f ♭ ⋆⟨ C ⟩ G ⟪ k ⟫) ♯ @@ -317,7 +317,7 @@ module _ (F : Functor C D) (G : Functor D C) where commInD f = (D .⋆IdL _) ∙ sym (D .⋆IdR _) sharpen1 : ∀ {x y} (f : C [ x , y ]) → F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ≡ F ⟪ f ⟫ ⋆⟨ D ⟩ D .id ♭ ♯ - sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .leftInv _)) + sharpen1 f = cong (λ v → F ⟪ f ⟫ ⋆⟨ D ⟩ v) (sym (adjIso .ret _)) η' : 𝟙⟨ C ⟩ ⇒ G ∘F F η' .N-ob x = D .id ♭ @@ -330,7 +330,7 @@ module _ (F : Functor C D) (G : Functor D C) where commInC g = (C .⋆IdL _) ∙ sym (C .⋆IdR _) sharpen2 : ∀ {x y} (g : D [ x , y ]) → C .id ♯ ♭ ⋆⟨ C ⟩ G ⟪ g ⟫ ≡ C .id ⋆⟨ C ⟩ G ⟪ g ⟫ - sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .rightInv _) + sharpen2 g = cong (λ v → v ⋆⟨ C ⟩ G ⟪ g ⟫) (adjIso .sec _) ε' : F ∘F G ⇒ 𝟙⟨ D ⟩ ε' .N-ob x = C .id ♯ @@ -371,7 +371,7 @@ module _ (F : Functor C D) (G : Functor D C) where -- takes g to Fg postcomposed with the counit adj→adj' .adjIso {d = d} .inv g = F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ -- invertibility follows from the triangle identities - adj→adj' .adjIso {c = c} {d} .rightInv g + adj→adj' .adjIso {c = c} {d} .sec g = η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ⟫ ≡⟨ cong (λ v → η ⟦ c ⟧ ⋆⟨ C ⟩ v) (G .F-seq _ _) ⟩ η ⟦ c ⟧ ⋆⟨ C ⟩ (G ⟪ F ⟪ g ⟫ ⟫ ⋆⟨ C ⟩ G ⟪ ε ⟦ d ⟧ ⟫) @@ -390,7 +390,7 @@ module _ (F : Functor C D) (G : Functor D C) where where natu : η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ F ⟪ g ⟫ ⟫ ≡ g ⋆⟨ C ⟩ η ⟦ G ⟅ d ⟆ ⟧ natu = sym (η .N-hom _) - adj→adj' .adjIso {c = c} {d} .leftInv f + adj→adj' .adjIso {c = c} {d} .ret f = F ⟪ η ⟦ c ⟧ ⋆⟨ C ⟩ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ ≡⟨ cong (λ v → v ⋆⟨ D ⟩ ε ⟦ d ⟧) (F .F-seq _ _) ⟩ F ⟪ η ⟦ c ⟧ ⟫ ⋆⟨ D ⟩ F ⟪ G ⟪ f ⟫ ⟫ ⋆⟨ D ⟩ ε ⟦ d ⟧ diff --git a/Cubical/Categories/Category/Path.agda b/Cubical/Categories/Category/Path.agda index 9313937d50..dccac638fe 100644 --- a/Cubical/Categories/Category/Path.agda +++ b/Cubical/Categories/Category/Path.agda @@ -113,12 +113,12 @@ module _ {C C' : Category ℓ ℓ'} where CategoryPathIso : Iso (CategoryPath C C') (C ≡ C') Iso.fun CategoryPathIso = CategoryPath.mk≡ Iso.inv CategoryPathIso = ≡→CategoryPath - Iso.rightInv CategoryPathIso = CategoryPathIsoRightInv + Iso.sec CategoryPathIso = CategoryPathIsoRightInv - ob≡ (Iso.leftInv CategoryPathIso a i) = ob≡ a - Hom≡ (Iso.leftInv CategoryPathIso a i) = Hom≡ a - id≡ (Iso.leftInv CategoryPathIso a i) = id≡ a - ⋆≡ (Iso.leftInv CategoryPathIso a i) = ⋆≡ a + ob≡ (Iso.ret CategoryPathIso a i) = ob≡ a + Hom≡ (Iso.ret CategoryPathIso a i) = Hom≡ a + id≡ (Iso.ret CategoryPathIso a i) = id≡ a + ⋆≡ (Iso.ret CategoryPathIso a i) = ⋆≡ a CategoryPath≡ : (cp cp' : CategoryPath C C') → (p≡ : ob≡ cp ≡ ob≡ cp') → diff --git a/Cubical/Categories/Constructions/Slice/Base.agda b/Cubical/Categories/Constructions/Slice/Base.agda index e918fe469e..543a14a794 100644 --- a/Cubical/Categories/Constructions/Slice/Base.agda +++ b/Cubical/Categories/Constructions/Slice/Base.agda @@ -62,8 +62,8 @@ module _ {xf yg : SliceOb} where SOPathIsoPathΣ : Iso (xf ≡ yg) (Σ[ p ∈ x ≡ y ] PathP (λ i → C [ p i , c ]) f g) SOPathIsoPathΣ .fun p = (λ i → (p i) .S-ob) , (λ i → (p i) .S-arr) SOPathIsoPathΣ .inv (p , q) i = sliceob {p i} (q i) - SOPathIsoPathΣ .rightInv _ = refl - SOPathIsoPathΣ .leftInv _ = refl + SOPathIsoPathΣ .sec _ = refl + SOPathIsoPathΣ .ret _ = refl SOPath≃PathΣ = isoToEquiv SOPathIsoPathΣ @@ -110,8 +110,8 @@ SliceHom-Σ-Iso : ∀ {a b} → Iso (SliceHom a b) (Σ[ h ∈ C [ S-ob a , S-ob b ] ] h ⋆⟨ C ⟩ (S-arr b) ≡ S-arr a) SliceHom-Σ-Iso .fun (slicehom h c) = h , c SliceHom-Σ-Iso .inv (h , c) = slicehom h c -SliceHom-Σ-Iso .rightInv = λ x → refl -SliceHom-Σ-Iso .leftInv = λ x → refl +SliceHom-Σ-Iso .sec = λ x → refl +SliceHom-Σ-Iso .ret = λ x → refl -- Category definition @@ -235,7 +235,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where pToIBase = catiso (C .id) idx (C .⋆IdL idx) (C .⋆IdL idx) l≡pToI : l ≡ pathToIso {C = C} x≡y .snd .inv - l≡pToI i = pToIIso .rightInv extractIso (~ i) .snd .inv + l≡pToI i = pToIIso .sec extractIso (~ i) .snd .inv l≡id : PathP (λ i → C [ x≡y (~ i) , x ]) l (C .id) l≡id = l≡pToI ◁ pToI≡id @@ -243,8 +243,8 @@ module _ ⦃ isU : isUnivalent C ⦄ where lf≡f : PathP (λ i → C [ x≡y (~ i) , c ]) (l ⋆⟨ C ⟩ f) f lf≡f = (λ i → (l≡id i) ⋆⟨ C ⟩ f) ▷ C .⋆IdL _ - sIso .rightInv is@(kc , isiso lc s r) i = catiso (kc'≡kc i) (lc'≡lc i) (s'≡s i) (r'≡r i) - -- we prove rightInv using a combination of univalence and the fact that homs are an h-set + sIso .sec is@(kc , isiso lc s r) i = catiso (kc'≡kc i) (lc'≡lc i) (s'≡s i) (r'≡r i) + -- we prove sec using a combination of univalence and the fact that homs are an h-set where kc' = (sIso .fun) (sIso .inv is) .fst lc' = (sIso .fun) (sIso .inv is) .snd .inv @@ -261,7 +261,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- mor k'≡k : k' ≡ k - k'≡k i = (pToIIso .rightInv extractIso) i .fst + k'≡k i = (pToIIso .sec extractIso) i .fst kcom'≡kcom : PathP (λ j → (k'≡k j) ⋆⟨ C ⟩ g ≡ f) (kc' .S-comm) (kc .S-comm) kcom'≡kcom = isSetHomP1 {C = C} _ _ λ i → (k'≡k i) ⋆⟨ C ⟩ g @@ -271,7 +271,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- inv l'≡l : l' ≡ l - l'≡l i = (pToIIso .rightInv extractIso) i .snd .inv + l'≡l i = (pToIIso .sec extractIso) i .snd .inv lcom'≡lcom : PathP (λ j → (l'≡l j) ⋆⟨ C ⟩ f ≡ g) (lc' .S-comm) (lc .S-comm) lcom'≡lcom = isSetHomP1 {C = C} _ _ λ i → (l'≡l i) ⋆⟨ C ⟩ f @@ -291,7 +291,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where r'≡r : PathP (λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i ≡ SliceCat .id) r' r r'≡r = isSetHomP1 {C = SliceCat} _ _ λ i → kc'≡kc i ⋆⟨ SliceCat ⟩ lc'≡lc i - sIso .leftInv p = p'≡p + sIso .ret p = p'≡p -- to show that the round trip is equivalent to the identity -- we show that this is true for each component (S-ob, S-arr) -- and then combine @@ -335,7 +335,7 @@ module _ ⦃ isU : isUnivalent C ⦄ where -- apply univalence of C -- this gives us the first component that we want p'Ob≡pOb : p'Ob ≡ pOb - p'Ob≡pOb = ppp ∙ pToIIso .leftInv pOb + p'Ob≡pOb = ppp ∙ pToIIso .ret pOb -- isSetHom gives us the second component, path between morphisms p'Mor≡pMor : PathP (λ j → PathP (λ i → C [ (p'Ob≡pOb j) i , c ]) f g) p'Mor pMor diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda index d87fdc1850..459afa9cc9 100644 --- a/Cubical/Categories/Constructions/Slice/Functor.agda +++ b/Cubical/Categories/Constructions/Slice/Functor.agda @@ -88,9 +88,9 @@ module _ (Pbs : Pullbacks C) where in slicehom _ (sym p) inv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = slicehom _ $ AssocCong₂⋆R C (sym (pbCommutes)) ∙ cong (_⋆ᶜ 𝑓) o - rightInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = + sec (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = SliceHom-≡-intro' _ _ (pullbackArrowUnique (sym o) refl) - leftInv (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = + ret (adjIso ∑𝑓⊣𝑓＊) (slicehom h o) = let ((_ , (_ , q)) , _) = univProp _ _ _ in SliceHom-≡-intro' _ _ (sym q) adjNatInD ∑𝑓⊣𝑓＊ f k = SliceHom-≡-intro' _ _ $ @@ -129,8 +129,8 @@ module _ (Pbs : Pullbacks C) where inv (adjIso L/b⊣R/b) (slicehom _ p) = slicehom _ $ AssocCong₂⋆R D (sym (N-hom ε _)) ∙ cong (_⋆ᵈ _) (sym (F-seq L _ _) ∙ cong (L ⟪_⟫) p) - rightInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.rightInv _ - leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.leftInv _ + sec (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.sec _ + ret (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ aI.ret _ adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ sym (C .⋆Assoc _ _ _) adjNatInC L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ @@ -163,7 +163,7 @@ module _ (Pbs : Pullbacks C) where ∙∙ sym (F-seq L _ _) ∙∙ cong (L ⟪_⟫) s) - rightInv (adjIso L/b⊣R/b) h = SliceHom-≡-intro' _ _ $ + sec (adjIso L/b⊣R/b) h = SliceHom-≡-intro' _ _ $ let p₂ : ∀ {x} → η ⟦ _ ⟧ ⋆ᶜ R ⟪ L ⟪ x ⟫ ⋆⟨ D ⟩ ε ⟦ _ ⟧ ⟫ ≡ x p₂ = cong (_ ⋆ᶜ_) (F-seq R _ _) ∙ AssocCong₂⋆L C (sym (N-hom η _)) @@ -172,9 +172,9 @@ module _ (Pbs : Pullbacks C) where in pullbackArrowUnique (sym (S-comm h)) p₂ - leftInv (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ + ret (adjIso L/b⊣R/b) _ = SliceHom-≡-intro' _ _ $ cong ((_⋆ᵈ _) ∘ L ⟪_⟫) (sym (snd (snd (fst (univProp _ _ _))))) - ∙ aI.leftInv _ + ∙ aI.ret _ adjNatInD L/b⊣R/b _ _ = SliceHom-≡-intro' _ _ $ let (h , (u , v)) = univProp _ _ _ .fst (u' , v') = pbU _ diff --git a/Cubical/Categories/Equivalence/Properties.agda b/Cubical/Categories/Equivalence/Properties.agda index f69f1be368..ff77a6e1ff 100644 --- a/Cubical/Categories/Equivalence/Properties.agda +++ b/Cubical/Categories/Equivalence/Properties.agda @@ -139,17 +139,17 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} p : _ p i = comp - (λ j → D [ iso-ob .rightInv x (~ j) , iso-ob .rightInv x (~ j) ]) + (λ j → D [ iso-ob .sec x (~ j) , iso-ob .sec x (~ j) ]) (λ j → λ { (i = i0) → iso-hom .rightInv _ (D .id {x = x}) (~ j) - ; (i = i1) → D .id {x = iso-ob .rightInv x (~ j)} }) + ; (i = i1) → D .id {x = iso-ob .sec x (~ j)} }) (D .id {x = x}) w-inv .F-seq {x = x} {z = z} f g = isFullyFaithful→Faithful {F = F} fullfaith _ _ _ _ (p ∙ sym (F .F-seq _ _)) where p : _ p i = comp - (λ j → D [ iso-ob .rightInv x (~ j) , iso-ob .rightInv z (~ j) ]) + (λ j → D [ iso-ob .sec x (~ j) , iso-ob .sec z (~ j) ]) (λ j → λ { (i = i0) → iso-hom .rightInv _ (f ⋆⟨ D ⟩ g) (~ j) ; (i = i1) → iso-hom .rightInv _ f (~ j) ⋆⟨ D ⟩ iso-hom .rightInv _ g (~ j) }) diff --git a/Cubical/Categories/Equivalence/WeakEquivalence.agda b/Cubical/Categories/Equivalence/WeakEquivalence.agda index bc2316c632..bbdc299260 100644 --- a/Cubical/Categories/Equivalence/WeakEquivalence.agda +++ b/Cubical/Categories/Equivalence/WeakEquivalence.agda @@ -159,7 +159,7 @@ module _ IsoCategoryPath : Iso (WeakEquivalence C C') (CategoryPath C C') fun IsoCategoryPath = WeakEquivlance→CategoryPath ∘f isWeakEquiv inv IsoCategoryPath = ≡→WeakEquivlance ∘f mk≡ - rightInv IsoCategoryPath b = CategoryPath≡ + sec IsoCategoryPath b = CategoryPath≡ (WeakEquivlance→CategoryPath (isWeakEquiv (≡→WeakEquivlance (mk≡ b)))) b (λ i j → Glue (C' .Category.ob) {φ = ~ j ∨ j ∨ i} (λ _ → _ , equivPathP @@ -176,7 +176,7 @@ module _ (λ _ _ → idIsEquiv _) j x y } - leftInv IsoCategoryPath we = cong₂ weakEquivalence + ret IsoCategoryPath we = cong₂ weakEquivalence (Functor≡ (transportRefl ∘f (F-ob (func we))) λ {c} {c'} f → (λ j → transport (λ i → HomPathP (isWeakEquiv we) i diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda index 4c658b965c..e03565cee3 100644 --- a/Cubical/Categories/Functor/Base.agda +++ b/Cubical/Categories/Functor/Base.agda @@ -171,8 +171,8 @@ open Iso Iso^opF : Iso (Functor C D) (Functor (C ^op) (D ^op)) Iso^opF .fun = _^opF Iso^opF .inv = _^opF⁻ -Iso^opF .rightInv F = Functor≡ (λ _ → refl) (λ _ → refl) -Iso^opF .leftInv F = Functor≡ (λ _ → refl) (λ _ → refl) +Iso^opF .sec F = Functor≡ (λ _ → refl) (λ _ → refl) +Iso^opF .ret F = Functor≡ (λ _ → refl) (λ _ → refl) ^opFEquiv : Functor C D ≃ Functor (C ^op) (D ^op) ^opFEquiv = isoToEquiv Iso^opF diff --git a/Cubical/Categories/Functor/Properties.agda b/Cubical/Categories/Functor/Properties.agda index 28749a8a0d..ce09c3c14e 100644 --- a/Cubical/Categories/Functor/Properties.agda +++ b/Cubical/Categories/Functor/Properties.agda @@ -98,15 +98,15 @@ isEquivFunctor≡ {C = C} {D = D} = Iso.isoToIsEquiv isom isom : Iso.Iso _ _ fun isom = _ inv isom x = (λ c i → F-ob (x i) c) , λ {c} {c'} f i → F-hom (x i) {c} {c'} f - F-ob (rightInv isom b _ i₁) = F-ob (b i₁) - F-hom (rightInv isom b _ i₁) = F-hom (b i₁) - F-id (rightInv isom b i i₁) = isProp→SquareP + F-ob (sec isom b _ i₁) = F-ob (b i₁) + F-hom (sec isom b _ i₁) = F-hom (b i₁) + F-id (sec isom b i i₁) = isProp→SquareP (λ i i₁ → D .isSetHom (F-hom (b i₁) (C .id)) (D .id)) refl refl (isProp→PathP (λ j → isSetHom D _ _) _ _) (λ i₁ → F-id (b i₁)) i i₁ - F-seq (rightInv isom b i i₁) f g = isProp→SquareP + F-seq (sec isom b i i₁) f g = isProp→SquareP (λ i i₁ → D .isSetHom (F-hom (b i₁) _) (seq' D (F-hom (b i₁) f) _)) refl refl (isProp→PathP (λ j → isSetHom D _ _) _ _) (λ i₁ → F-seq (b i₁) f g) i i₁ - leftInv isom _ = refl + ret isom _ = refl isOfHLevelFunctor : ∀ hLevel → isOfHLevel (2 + hLevel) (D .ob) → isOfHLevel (2 + hLevel) (Functor C D) diff --git a/Cubical/Categories/Instances/CommRings.agda b/Cubical/Categories/Instances/CommRings.agda index a570a9792a..45ad5287f2 100644 --- a/Cubical/Categories/Instances/CommRings.agda +++ b/Cubical/Categories/Instances/CommRings.agda @@ -61,24 +61,24 @@ CommRingIsoIsoCatIso : {R S : CommRing ℓ} → Iso (CommRingIso R S) (CatIso Co (fun CommRingIsoIsoCatIso e) .fst = (e .fst .fun) , (e .snd) (fun (CommRingIsoIsoCatIso {R = R} {S}) e) .snd .inv = e .fst .inv - , makeIsCommRingHom (sym (cong (e .fst .inv) (pres1 (e .snd))) ∙ e .fst .leftInv _) - (λ x y → let rem = e .fst .rightInv _ - ∙∙ (λ i → S .snd ._+_ (e .fst .rightInv x (~ i)) (e .fst .rightInv y (~ i))) + , makeIsCommRingHom (sym (cong (e .fst .inv) (pres1 (e .snd))) ∙ e .fst .ret _) + (λ x y → let rem = e .fst .sec _ + ∙∙ (λ i → S .snd ._+_ (e .fst .sec x (~ i)) (e .fst .sec y (~ i))) ∙∙ sym (pres+ (e .snd) _ _) in injCommRingIso {R = R} {S} e _ _ rem) - (λ x y → let rem = e .fst .rightInv _ - ∙∙ (λ i → S .snd ._·_ (e .fst .rightInv x (~ i)) (e .fst .rightInv y (~ i))) + (λ x y → let rem = e .fst .sec _ + ∙∙ (λ i → S .snd ._·_ (e .fst .sec x (~ i)) (e .fst .sec y (~ i))) ∙∙ sym (pres· (e .snd) _ _) in injCommRingIso {R = R} {S} e _ _ rem) -(fun CommRingIsoIsoCatIso e) .snd .sec = CommRingHom≡ (funExt (e .fst .rightInv)) -(fun CommRingIsoIsoCatIso e) .snd .ret = CommRingHom≡ (funExt (e .fst .leftInv)) +(fun CommRingIsoIsoCatIso e) .snd .sec = CommRingHom≡ (funExt (e .fst .sec)) +(fun CommRingIsoIsoCatIso e) .snd .ret = CommRingHom≡ (funExt (e .fst .ret)) fun (fst (inv CommRingIsoIsoCatIso e)) = e .fst .fst inv (fst (inv CommRingIsoIsoCatIso e)) = e .snd .inv .fst -rightInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .sec i) x -leftInv (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .ret i) x +sec (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .sec i) x +ret (fst (inv CommRingIsoIsoCatIso e)) x i = fst (e .snd .ret i) x snd (inv CommRingIsoIsoCatIso e) = e .fst .snd -rightInv CommRingIsoIsoCatIso x = CatIso≡ _ _ (CommRingHom≡ refl) -leftInv (CommRingIsoIsoCatIso {R = R} {S}) x = +sec CommRingIsoIsoCatIso x = CatIso≡ _ _ (CommRingHom≡ refl) +ret (CommRingIsoIsoCatIso {R = R} {S}) x = Σ≡Prop (λ x → isPropIsCommRingHom (R .snd) (x .fun) (S .snd)) diff --git a/Cubical/Categories/Instances/EilenbergMoore.agda b/Cubical/Categories/Instances/EilenbergMoore.agda index b129138461..715b92955b 100644 --- a/Cubical/Categories/Instances/EilenbergMoore.agda +++ b/Cubical/Categories/Instances/EilenbergMoore.agda @@ -110,7 +110,7 @@ module _ {C : Category ℓC ℓC'} (monadM : Monad C) where ((F-hom M (F-hom M f) C.⋆ F-hom M β) C.⋆ β) ≡⟨ cong (C._⋆ β) (sym (F-seq M _ _)) ⟩ (F-hom M (F-hom M f C.⋆ β) C.⋆ β) ∎ - rightInv (emBijection a (algebra b β , isEMB)) f = + sec (emBijection a (algebra b β , isEMB)) f = (N-ob η a C.⋆ (F-hom M f C.⋆ β)) ≡⟨ sym (C.⋆Assoc _ _ _) ⟩ ((N-ob η a C.⋆ F-hom M f) C.⋆ β) @@ -122,7 +122,7 @@ module _ {C : Category ℓC ℓC'} (monadM : Monad C) where (f C.⋆ C.id) ≡⟨ C.⋆IdR _ ⟩ f ∎ - leftInv (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = AlgebraHom≡ M ( + ret (emBijection a (algebra b β , isEMB)) (algebraHom f isalgF) = AlgebraHom≡ M ( (F-hom M (N-ob η a C.⋆ f) C.⋆ β) ≡⟨ cong (C._⋆ β) (F-seq M _ _) ⟩ ((F-hom M (N-ob η a) C.⋆ F-hom M f) C.⋆ β) diff --git a/Cubical/Categories/Instances/FunctorAlgebras.agda b/Cubical/Categories/Instances/FunctorAlgebras.agda index 9c2e4f2260..e070abb32d 100644 --- a/Cubical/Categories/Instances/FunctorAlgebras.agda +++ b/Cubical/Categories/Instances/FunctorAlgebras.agda @@ -46,8 +46,8 @@ module _ {C : Category ℓC ℓC'} (F : Functor C C) where isoRepAlgebraHom : (algA algB : Algebra) → AlgebraHom algA algB ≅ RepAlgebraHom algA algB fun (isoRepAlgebraHom algA algB) (algebraHom f isalgF) = f , isalgF inv (isoRepAlgebraHom algA algB) (f , isalgF) = algebraHom f isalgF - rightInv (isoRepAlgebraHom algA algB) (f , isalgF) = refl - leftInv (isoRepAlgebraHom algA algB) (algebraHom f isalgF)= refl + sec (isoRepAlgebraHom algA algB) (f , isalgF) = refl + ret (isoRepAlgebraHom algA algB) (algebraHom f isalgF)= refl pathRepAlgebraHom : (algA algB : Algebra) → AlgebraHom algA algB ≡ RepAlgebraHom algA algB pathRepAlgebraHom algA algB = ua (isoToEquiv (isoRepAlgebraHom algA algB)) diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda index 8e735ae52f..30f967ea9a 100644 --- a/Cubical/Categories/Instances/Functors.agda +++ b/Cubical/Categories/Instances/Functors.agda @@ -93,11 +93,11 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where Iso-FUNCTORIso-NatIso : {F G : Functor C D} → Iso (CatIso FUNCTOR F G) (NatIso F G) Iso-FUNCTORIso-NatIso .fun = FUNCTORIso→NatIso Iso-FUNCTORIso-NatIso .inv = NatIso→FUNCTORIso - Iso-FUNCTORIso-NatIso .rightInv α i .trans = α .trans - Iso-FUNCTORIso-NatIso .rightInv α i .nIso = + Iso-FUNCTORIso-NatIso .sec α i .trans = α .trans + Iso-FUNCTORIso-NatIso .sec α i .nIso = isProp→PathP (λ i → isPropΠ (λ _ → isPropIsIso _)) (FUNCTORIso' (α .trans) (FUNCTORIso _ (α .nIso))) (α .nIso) i - Iso-FUNCTORIso-NatIso .leftInv α i .fst = α .fst - Iso-FUNCTORIso-NatIso .leftInv α i .snd = + Iso-FUNCTORIso-NatIso .ret α i .fst = α .fst + Iso-FUNCTORIso-NatIso .ret α i .snd = isProp→PathP (λ i → isPropIsIso _) (FUNCTORIso _ (FUNCTORIso' _ (α .snd))) (α .snd) i FUNCTORIso≃NatIso : {F G : Functor C D} → CatIso FUNCTOR F G ≃ NatIso F G diff --git a/Cubical/Categories/Instances/Functors/Currying.agda b/Cubical/Categories/Instances/Functors/Currying.agda index 92ccde45e2..21fe9ffd9d 100644 --- a/Cubical/Categories/Instances/Functors/Currying.agda +++ b/Cubical/Categories/Instances/Functors/Currying.agda @@ -94,11 +94,11 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where isoλF : Iso (Functor (E ×C C) D) (Functor E (FUNCTOR C D)) fun isoλF = λF inv isoλF = λF⁻ - rightInv isoλF b = Functor≡ (λ _ → Functor≡ (λ _ → refl) + sec isoλF b = Functor≡ (λ _ → Functor≡ (λ _ → refl) λ _ → cong (seq' D _) (congS (flip N-ob _) (F-id b)) ∙ D .⋆IdR _) λ _ → makeNatTransPathP _ _ (funExt λ _ → cong (comp' D _) (F-id (F-ob b _)) ∙ D .⋆IdL _) - leftInv isoλF a = Functor≡ (λ _ → refl) λ _ → sym (F-seq a _ _) + ret isoλF a = Functor≡ (λ _ → refl) λ _ → sym (F-seq a _ _) ∙ cong (F-hom a) (cong₂ _,_ (E .⋆IdL _) (C .⋆IdR _)) open AdjointEquivalence diff --git a/Cubical/Categories/Instances/Groups.agda b/Cubical/Categories/Instances/Groups.agda index 658d2f06c8..66373c560d 100644 --- a/Cubical/Categories/Instances/Groups.agda +++ b/Cubical/Categories/Instances/Groups.agda @@ -52,8 +52,8 @@ module _ {ℓ : Level} where →iso : ∀ {x} → isCatIso GroupCategory x → Iso _ _ fun (→iso ici) = _ inv (→iso ici) = fst (inv ici) - rightInv (→iso ici) b i = fst (sec ici i) b - leftInv (→iso ici) a i = fst (ret ici i) a + sec (→iso ici) b i = fst (sec ici i) b + ret (→iso ici) a i = fst (ret ici i) a →ciso : ∀ {x} → isEquiv (fst x) → isCatIso GroupCategory x fst (inv (→ciso is≃)) = _ diff --git a/Cubical/Categories/Instances/Sets.agda b/Cubical/Categories/Instances/Sets.agda index aab7f9b501..d5dc99a87d 100644 --- a/Cubical/Categories/Instances/Sets.agda +++ b/Cubical/Categories/Instances/Sets.agda @@ -63,8 +63,8 @@ module _ {ℓ ℓ' : Level} where (Lift {ℓ}{ℓ'} (X .fst) → Lift {ℓ}{ℓ'} (Y .fst)) fun LiftFIso = LiftF .F-hom {X} {Y} inv LiftFIso = λ f x → f (lift x) .lower - rightInv LiftFIso = λ _ → funExt λ _ → refl - leftInv LiftFIso = λ _ → funExt λ _ → refl + sec LiftFIso = λ _ → funExt λ _ → refl + ret LiftFIso = λ _ → funExt λ _ → refl module _ {C : Category ℓ ℓ'} {F : Functor C (SET ℓ')} where open NatTrans @@ -94,25 +94,25 @@ module _ {A B : (SET ℓ) .ob } where → CatIso (SET ℓ) A B Iso→CatIso is .fst = is .fun Iso→CatIso is .snd .cInv = is .inv - Iso→CatIso is .snd .sec = funExt λ b → is .rightInv b -- is .rightInv - Iso→CatIso is .snd .ret = funExt λ b → is .leftInv b -- is .rightInv + Iso→CatIso is .snd .sec = funExt λ b → is .sec b -- is .sec + Iso→CatIso is .snd .ret = funExt λ b → is .ret b -- is .sec CatIso→Iso : CatIso (SET ℓ) A B → Iso (fst A) (fst B) CatIso→Iso cis .fun = cis .fst CatIso→Iso cis .inv = cis .snd .cInv - CatIso→Iso cis .rightInv = funExt⁻ λ b → cis .snd .sec b - CatIso→Iso cis .leftInv = funExt⁻ λ b → cis .snd .ret b + CatIso→Iso cis .sec = funExt⁻ λ b → cis .snd .sec b + CatIso→Iso cis .ret = funExt⁻ λ b → cis .snd .ret b Iso-Iso-CatIso : Iso (Iso (fst A) (fst B)) (CatIso (SET ℓ) A B) fun Iso-Iso-CatIso = Iso→CatIso inv Iso-Iso-CatIso = CatIso→Iso - rightInv Iso-Iso-CatIso b = refl - fun (leftInv Iso-Iso-CatIso a i) = fun a - inv (leftInv Iso-Iso-CatIso a i) = inv a - rightInv (leftInv Iso-Iso-CatIso a i) = rightInv a - leftInv (leftInv Iso-Iso-CatIso a i) = leftInv a + sec Iso-Iso-CatIso b = refl + fun (ret Iso-Iso-CatIso a i) = fun a + inv (ret Iso-Iso-CatIso a i) = inv a + sec (ret Iso-Iso-CatIso a i) = sec a + ret (ret Iso-Iso-CatIso a i) = ret a Iso-CatIso-≡ : Iso (CatIso (SET ℓ) A B) (A ≡ B) Iso-CatIso-≡ = compIso (invIso Iso-Iso-CatIso) (hSet-Iso-Iso-≡ _ _) diff --git a/Cubical/Categories/Limits/Initial.agda b/Cubical/Categories/Limits/Initial.agda index 6d53df07be..8b97c8e00a 100644 --- a/Cubical/Categories/Limits/Initial.agda +++ b/Cubical/Categories/Limits/Initial.agda @@ -79,5 +79,5 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} (F : Functor C D) w _♯ F⊣G (fst (initX (F-ob G y))) ≡⟨ cong (F⊣G ♯) (snd (initX (F-ob G y)) (_♭ F⊣G ψ)) ⟩ _♯ F⊣G (_♭ F⊣G ψ) - ≡⟨ leftInv (adjIso F⊣G) ψ ⟩ + ≡⟨ ret (adjIso F⊣G) ψ ⟩ ψ ∎ diff --git a/Cubical/Categories/NaturalTransformation/Properties.agda b/Cubical/Categories/NaturalTransformation/Properties.agda index 206ea5639c..f5c92f490f 100644 --- a/Cubical/Categories/NaturalTransformation/Properties.agda +++ b/Cubical/Categories/NaturalTransformation/Properties.agda @@ -60,8 +60,8 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where NatTransIsoΣ : Iso (NatTrans F G) NatTransΣ NatTransIsoΣ .fun (natTrans N-ob N-hom) = N-ob , N-hom NatTransIsoΣ .inv (N-ob , N-hom) = (natTrans N-ob N-hom) - NatTransIsoΣ .rightInv _ = refl - NatTransIsoΣ .leftInv _ = refl + NatTransIsoΣ .sec _ = refl + NatTransIsoΣ .ret _ = refl NatTrans≡Σ : NatTrans F G ≡ NatTransΣ NatTrans≡Σ = isoToPath NatTransIsoΣ @@ -90,8 +90,8 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where βHom)) NTPathIsoPathΣ .fun p = (λ i → p i .N-ob) , (λ i → p i .N-hom) NTPathIsoPathΣ .inv (po , ph) i = record { N-ob = po i ; N-hom = ph i } - NTPathIsoPathΣ .rightInv pσ = refl - NTPathIsoPathΣ .leftInv p = refl + NTPathIsoPathΣ .sec pσ = refl + NTPathIsoPathΣ .ret p = refl NTPath≃PathΣ = isoToEquiv NTPathIsoPathΣ @@ -102,7 +102,7 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} where isSetNatTrans : {F G : Functor C D} → isSet (NatTrans F G) isSetNatTrans = - isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (leftInv NatTransIsoΣ) + isSetRetract (fun NatTransIsoΣ) (inv NatTransIsoΣ) (ret NatTransIsoΣ) (isSetΣSndProp (isSetΠ (λ _ → isSetHom D)) (λ _ → isPropImplicitΠ2 (λ _ _ → isPropΠ (λ _ → isSetHom D _ _)))) @@ -180,8 +180,8 @@ module _ {B : Category ℓB ℓB'}{C : Category ℓC ℓC'}{D : Category ℓD N-ob (fun ⇒^opFiso x) = N-ob x N-hom (fun ⇒^opFiso x) f = sym (N-hom x f) inv ⇒^opFiso = _ -rightInv ⇒^opFiso _ = refl -leftInv ⇒^opFiso _ = refl +sec ⇒^opFiso _ = refl +ret ⇒^opFiso _ = refl congNatIso^opFiso : Iso (F ≅ᶜ F') (_^opF {C = C} {D = D} F' ≅ᶜ F ^opF ) trans (fun congNatIso^opFiso x) = Iso.fun ⇒^opFiso (trans x) @@ -189,6 +189,6 @@ inv (nIso (fun congNatIso^opFiso x) x₁) = _ sec (nIso (fun congNatIso^opFiso x) x₁) = ret (nIso x x₁) ret (nIso (fun congNatIso^opFiso x) x₁) = sec (nIso x x₁) inv congNatIso^opFiso = _ -rightInv congNatIso^opFiso _ = refl -leftInv congNatIso^opFiso _ = refl +sec congNatIso^opFiso _ = refl +ret congNatIso^opFiso _ = refl diff --git a/Cubical/Categories/Presheaf/Properties.agda b/Cubical/Categories/Presheaf/Properties.agda index 221a844b79..01b0f7aac2 100644 --- a/Cubical/Categories/Presheaf/Properties.agda +++ b/Cubical/Categories/Presheaf/Properties.agda @@ -241,11 +241,11 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) → Iso A (Σ[ b ∈ B ] fiber ϕ b) typeSectionIso ϕ .fun a = (ϕ a) , (a , refl) typeSectionIso ϕ .inv (b , (a , eq)) = a - typeSectionIso {isSetB = isSetB} ϕ .rightInv (b , (a , eq)) + typeSectionIso {isSetB = isSetB} ϕ .sec (b , (a , eq)) = ΣPathP (eq , ΣPathP (refl , isOfHLevel→isOfHLevelDep 1 (λ b' → isSetB _ _) refl eq eq)) - typeSectionIso ϕ .leftInv a = refl + typeSectionIso ϕ .ret a = refl -- the natural transformation -- just applies typeSectionIso @@ -294,9 +294,9 @@ module _ {ℓS : Level} (C : Category ℓ ℓ') (F : Functor (C ^op) (SET ℓS)) → Iso (B x) (fiber {A = Σ[ a ∈ A ] B a} (λ (x , _) → x) x) typeFiberIso {x = x} _ .fun b = (x , b) , refl typeFiberIso _ .inv ((a , b) , eq) = subst _ eq b - typeFiberIso {isSetA = isSetA} {x = x} B .rightInv ((a , b) , eq) + typeFiberIso {isSetA = isSetA} {x = x} B .sec ((a , b) , eq) = fibersEqIfRepsEq {isSetB = isSetA} (λ (x , _) → x) (ΣPathP (sym eq , symP (transport-filler (λ i → B (eq i)) b))) - typeFiberIso {x = x} _ .leftInv b = sym (transport-filler refl b) + typeFiberIso {x = x} _ .ret b = sym (transport-filler refl b) -- the natural isomorphism -- applies typeFiberIso (inv) diff --git a/Cubical/Categories/Presheaf/Representable.agda b/Cubical/Categories/Presheaf/Representable.agda index 910a9d1764..dc005f1068 100644 --- a/Cubical/Categories/Presheaf/Representable.agda +++ b/Cubical/Categories/Presheaf/Representable.agda @@ -111,15 +111,15 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where (lift f) .lower) lem = funExt (λ f i → (yonedaᴾ* {C = C} P (repr .fst) - .Iso.leftInv (repr .snd .trans) (~ i) ⟦ A ⟧) + .Iso.ret (repr .snd .trans) (~ i) ⟦ A ⟧) (lift f) .lower) anIso : Iso (C [ A , repr .fst ]) (fst (Functor.F-ob P A)) anIso .Iso.fun f = (repr .snd .trans ⟦ A ⟧) (lift f) .lower anIso .Iso.inv p = repr .snd .nIso A .inv (lift p) .lower - anIso .Iso.rightInv b = + anIso .Iso.sec b = cong lower (funExt⁻ (repr .snd .nIso A .sec) (lift b)) - anIso .Iso.leftInv a = + anIso .Iso.ret a = cong lower (funExt⁻ (repr .snd .nIso A .ret) (lift a)) universalElementToRepresentation : UniversalElement → Representation @@ -136,14 +136,14 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where Representation≅UniversalElement : Iso Representation UniversalElement Representation≅UniversalElement .Iso.fun = representationToUniversalElement Representation≅UniversalElement .Iso.inv = universalElementToRepresentation - Representation≅UniversalElement .Iso.rightInv η = + Representation≅UniversalElement .Iso.sec η = isoFunInjective UniversalElementIsoΣ _ _ (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) - (yonedaᴾ* {C = C} P (η .vertex) .Iso.rightInv (η .element))))) - Representation≅UniversalElement .Iso.leftInv repr = + (yonedaᴾ* {C = C} P (η .vertex) .Iso.sec (η .element))))) + Representation≅UniversalElement .Iso.ret repr = ΣPathP (refl , (NatIso≡ (cong NatTrans.N-ob - (yonedaᴾ* {C = C} P (repr .fst) .Iso.leftInv (repr .snd .trans))))) + (yonedaᴾ* {C = C} P (repr .fst) .Iso.ret (repr .snd .trans))))) isTerminalToIsUniversal : ∀ {η : Elementᴾ {C = C} P} → isTerminal Elements η → isUniversal (η .fst) (η .snd) @@ -183,10 +183,10 @@ module _ {ℓo}{ℓh}{ℓp} (C : Category ℓo ℓh) (P : Presheaf C ℓp) where TerminalElement≅UniversalElement : Iso TerminalElement UniversalElement TerminalElement≅UniversalElement .Iso.fun = terminalElementToUniversalElement TerminalElement≅UniversalElement .Iso.inv = universalElementToTerminalElement - TerminalElement≅UniversalElement .Iso.rightInv η = + TerminalElement≅UniversalElement .Iso.sec η = isoFunInjective UniversalElementIsoΣ _ _ (ΣPathP (refl , (Σ≡Prop (λ _ → isPropIsUniversal _ _) refl))) - TerminalElement≅UniversalElement .Iso.leftInv η = + TerminalElement≅UniversalElement .Iso.ret η = Σ≡Prop (isPropIsTerminal Elements) refl Representation≅TerminalElement : Iso Representation TerminalElement diff --git a/Cubical/Categories/RezkCompletion/Construction.agda b/Cubical/Categories/RezkCompletion/Construction.agda index 1af07e349c..6892d1acb1 100644 --- a/Cubical/Categories/RezkCompletion/Construction.agda +++ b/Cubical/Categories/RezkCompletion/Construction.agda @@ -219,15 +219,15 @@ module RezkByHIT (C : Category ℓ ℓ') where H-inc-ua f = TypeOfHLevel≡ 2 $ isoToPath λ where .Iso.fun → C._⋆ f .fst .Iso.inv → C._⋆ f .snd .inv - .Iso.rightInv _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .sec) ∙∙ C.⋆IdR _ - .Iso.leftInv _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .ret) ∙∙ C.⋆IdR _ + .Iso.sec _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .sec) ∙∙ C.⋆IdR _ + .Iso.ret _ → C.⋆Assoc _ _ _ ∙∙ congR C._⋆_ (f .snd .ret) ∙∙ C.⋆IdR _ H-ua-inc : ∀ {x y z} → IsoC x y → H-inc x z ≡ H-inc y z H-ua-inc f = TypeOfHLevel≡ 2 $ isoToPath λ where .Iso.fun → f .snd .inv C.⋆_ .Iso.inv → f .fst C.⋆_ - .Iso.rightInv _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .sec) ∙∙ C.⋆IdL _ - .Iso.leftInv _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .ret) ∙∙ C.⋆IdL _ + .Iso.sec _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .sec) ∙∙ C.⋆IdL _ + .Iso.ret _ → sym (C.⋆Assoc _ _ _) ∙∙ congL C._⋆_ (f .snd .ret) ∙∙ C.⋆IdL _ typeSquare : ∀ {A B C D : Type ℓ''} {P : A ≡ B} {Q : C ≡ D} {R S} → (∀ x → transport S (transport P x) ≡ transport Q (transport R x)) diff --git a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda index 92cb955d58..473c1a0a1a 100644 --- a/Cubical/Categories/Site/Instances/ZariskiCommRing.agda +++ b/Cubical/Categories/Site/Instances/ZariskiCommRing.agda @@ -208,7 +208,7 @@ isSubcanonicalZariskiCoverage A R (unimodvec n f isUniModF) = isoToIsEquiv theIs (CompatibleFamily (yo A) (str (covers zariskiCoverage R) um)) fun theIso = elementToCompatibleFamily _ _ inv theIso fam = inducedHom f isUniModF fam - rightInv theIso fam = CompatibleFamily≡ _ _ _ _ + sec theIso fam = CompatibleFamily≡ _ _ _ _ λ i → CommRingHom≡ (funExt λ a → applyEqualizerLemma f isUniModF fam a .fst .snd i) - leftInv theIso φ = inducedHomUnique _ _ _ _ λ _ _ → refl + ret theIso φ = inducedHomUnique _ _ _ _ λ _ _ → refl diff --git a/Cubical/Categories/Yoneda.agda b/Cubical/Categories/Yoneda.agda index a32f3849ca..daccf976c6 100644 --- a/Cubical/Categories/Yoneda.agda +++ b/Cubical/Categories/Yoneda.agda @@ -56,8 +56,8 @@ module _ {C : Category ℓ ℓ'} where theIso : Iso natType setType theIso .fun = ϕ theIso .inv = Ψ - theIso .rightInv x i = F .F-id i x - theIso .leftInv α@(natTrans αo αh) = + theIso .sec x i = F .F-id i x + theIso .ret α@(natTrans αo αh) = NatTrans-≡-intro (sym αo≡βo) (symP αh≡βh) where β = Ψ (ϕ α) @@ -178,8 +178,8 @@ yoneda* {ℓ}{ℓ'}{ℓ''}{C} F c = the-iso .fun α .N-hom g = α .N-hom (g .lower) the-iso .inv β .N-ob d f = β .N-ob d f the-iso .inv β .N-hom g = β .N-hom (lift g) - the-iso .rightInv β = refl - the-iso .leftInv α = refl + the-iso .sec β = refl + the-iso .ret α = refl yonedaᴾ* : {C : Category ℓ ℓ'}(F : Functor (C ^op) (SET ℓ'')) → (c : Category.ob C) @@ -204,8 +204,8 @@ yonedaᴾ* {ℓ}{ℓ'}{ℓ''}{C} F c = the-iso .fun α .N-hom = α .N-hom the-iso .inv β .N-ob = β .N-ob the-iso .inv β .N-hom = β .N-hom - the-iso .rightInv = λ b → refl - the-iso .leftInv = λ a → refl + the-iso .sec = λ b → refl + the-iso .ret = λ a → refl -- Yoneda embedding -- TODO: probably want to rename/refactor @@ -236,8 +236,8 @@ module _ {C : Category ℓ ℓ'} where yoIso : Iso (NatTrans (yo x) F) (F .F-ob x .fst) yoIso .Iso.fun = yo-yo-yo yoIso .Iso.inv = no-no-no - yoIso .Iso.rightInv b i = F .F-id i b - yoIso .Iso.leftInv a = makeNatTransPath (funExt λ _ → funExt rem) + yoIso .Iso.sec b i = F .F-id i b + yoIso .Iso.ret a = makeNatTransPath (funExt λ _ → funExt rem) where rem : ∀ {z} (x₁ : C [ z , x ]) → F .F-hom x₁ (yo-yo-yo a) ≡ (a .N-ob z) x₁ rem g = @@ -253,7 +253,7 @@ module _ {C : Category ℓ ℓ'} where isFullYO : isFull YO - isFullYO x y F[f] = ∣ yo-yo-yo _ F[f] , yoIso {x} (yo y) .Iso.leftInv F[f] ∣₁ + isFullYO x y F[f] = ∣ yo-yo-yo _ F[f] , yoIso {x} (yo y) .Iso.ret F[f] ∣₁ isFaithfulYO : isFaithful YO isFaithfulYO x y f g p i = diff --git a/Cubical/Codata/Conat/Bounded.agda b/Cubical/Codata/Conat/Bounded.agda index a5f8e0322b..7b120d9252 100644 --- a/Cubical/Codata/Conat/Bounded.agda +++ b/Cubical/Codata/Conat/Bounded.agda @@ -100,8 +100,8 @@ discreteB′ m (i , i≺m) (j , j≺m) with discreteℕ i j Σ≺∞≃ℕ = isoToEquiv λ where .fun → fst .inv n → n , ≺∞ n - .rightInv _ → refl - .leftInv (n , p) i → λ where + .sec _ → refl + .ret (n , p) i → λ where .fst → n .snd → isProp≺ n ∞ (≺∞ n) p i where open Iso @@ -225,14 +225,14 @@ module Untangle iso- : Iso (Bounded m) (Bounded n) iso- .fun = f- iso- .inv = g- - iso- .rightInv = f-g- - iso- .leftInv = g-f- + iso- .sec = f-g- + iso- .ret = g-f- untangled : ∀{m n} → Iso (Bounded′ (csuc m)) (Bounded′ (csuc n)) → Iso (Bounded m) (Bounded n) -untangled isom = Untangle.iso- fun inv rightInv leftInv +untangled isom = Untangle.iso- fun inv sec ret where open Iso isom Bounded-inj-iso : ∀ m n → Iso (Bounded m) (Bounded n) → m ≡ n diff --git a/Cubical/Codata/Containers/Coalgebras.agda b/Cubical/Codata/Containers/Coalgebras.agda index af71cd7963..9be4b72345 100644 --- a/Cubical/Codata/Containers/Coalgebras.agda +++ b/Cubical/Codata/Containers/Coalgebras.agda @@ -24,5 +24,5 @@ module Coalgs (S : Type ℓ) (Q : S → Type ℓ') where isom : Iso (Σ[ s ∈ S ] (Q s → M S Q)) (M S Q) fun isom = uncurry sup-M inv isom m = shape m , pos m - rightInv isom m = ηEqM m - leftInv isom (s , f) = refl + sec isom m = ηEqM m + ret isom (s , f) = refl diff --git a/Cubical/Codata/M/M/Base.agda b/Cubical/Codata/M/M/Base.agda index 44361a55aa..a7cb24642b 100644 --- a/Cubical/Codata/M/M/Base.agda +++ b/Cubical/Codata/M/M/Base.agda @@ -44,8 +44,8 @@ lemma11-Iso : (X 0) fun (lemma11-Iso X l) (x , y) = x 0 inv (lemma11-Iso {S = S} X l) x₀ = limit-collapse {S = S} X l x₀ , (λ n → refl {x = limit-collapse {S = S} X l x₀ (suc n)}) -rightInv (lemma11-Iso X l) _ = refl -leftInv (lemma11-Iso {ℓ = ℓ} {S = S} X l) (x , y) i = +sec (lemma11-Iso X l) _ = refl +ret (lemma11-Iso {ℓ = ℓ} {S = S} X l) (x , y) i = let temp = χ-prop (x 0) (fst (inv (lemma11-Iso {S = S} X l) (fun (lemma11-Iso {S = S} X l) (x , y))) , refl , (λ n → refl {x = limit-collapse {S = S} X l (x 0) (suc n)})) (x , refl , y) in temp i .fst , proj₂ (temp i .snd) where @@ -63,8 +63,8 @@ leftInv (lemma11-Iso {ℓ = ℓ} {S = S} X l) (x , y) i = (NatSection (X-fiber-over-ℕ x₀)) fun (Z-is-Section x₀) (x , (z , y)) = record { section = x ; sec-comm-zero = z ; sec-comm-suc = y } inv (Z-is-Section x₀) x = NatSection.section x , (sec-comm-zero x , sec-comm-suc x) - rightInv (Z-is-Section x₀) _ = refl - leftInv (Z-is-Section x₀) (x , (z , y)) = refl + sec (Z-is-Section x₀) _ = refl + ret (Z-is-Section x₀) (x , (z , y)) = refl -- S≡T χ-prop' : (x₀ : X 0) → isProp (NatSection (X-fiber-over-ℕ x₀)) @@ -159,11 +159,11 @@ shift-iso S@(A , B) = (limit-of-chain (sequence S)) fun α-iso-step-1-4-Iso-lem-12 (a , b) = (λ { 0 → lift tt ; (suc n) → (a .fst n) , (b .fst n)}) , λ { 0 → refl {x = lift tt} ; (suc m) i → a .snd m i , b .snd m i } inv α-iso-step-1-4-Iso-lem-12 x = ((λ n → (x .fst) (suc n) .fst) , λ n i → (x .snd) (suc n) i .fst) , (λ n → (x .fst) (suc n) .snd) , λ n i → (x .snd) (suc n) i .snd - fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = lift tt - fst (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = refl i - snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = refl - snd (rightInv α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = c (suc n) - leftInv α-iso-step-1-4-Iso-lem-12 (a , b) = refl + fst (sec α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = lift tt + fst (sec α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = refl i + snd (sec α-iso-step-1-4-Iso-lem-12 (b , c) i) 0 = refl + snd (sec α-iso-step-1-4-Iso-lem-12 (b , c) i) (suc n) = c (suc n) + ret α-iso-step-1-4-Iso-lem-12 (a , b) = refl shift : ∀ {ℓ} (S : Container ℓ) -> P₀ S (M S) ≡ M S shift S = isoToPath (shift-iso S) -- lemma 13 & lemma 12 diff --git a/Cubical/Codata/M/M/Properties.agda b/Cubical/Codata/M/M/Properties.agda index 6225bbbdcd..e26c818708 100644 --- a/Cubical/Codata/M/M/Properties.agda +++ b/Cubical/Codata/M/M/Properties.agda @@ -32,14 +32,14 @@ in-inverse-out {S = S} = subst (λ inv → in-fun {S = S} ∘ inv ≡ idfun (M S -- substituting refl makes type-checking work a lot faster, but introduces a transport -- TODO (2020-05-23): revisit this at some point to see if it's still needed in future versions of agda def : (in-fun {S = S} ∘ inv (shift-iso S)) ≡ idfun (M S) - def = funExt (rightInv (shift-iso S)) + def = funExt (sec (shift-iso S)) idpath : inv (shift-iso S) ≡ out-fun {S = S} idpath = refl out-inverse-in : ∀ {ℓ} {S : Container ℓ} → (out-fun {S = S} ∘ in-fun {S = S}) ≡ idfun (P₀ S (M S)) out-inverse-in {S = S} = subst (λ fun → out-fun {S = S} ∘ fun ≡ idfun (P₀ S (M S))) idpath def where def : (out-fun {S = S} ∘ fun (shift-iso S)) ≡ idfun (P₀ S (M S)) - def = funExt (leftInv (shift-iso S)) + def = funExt (ret (shift-iso S)) idpath : fun (shift-iso S) ≡ in-fun {S = S} idpath = refl diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda index 2bc115cb30..b0503c0b88 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Base.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda @@ -260,14 +260,14 @@ coHom≅coHomRed n G A = Iso.fun (fst main) = ST.map fst Iso.inv (fst main) = ST.map λ f → (λ x → f x -ₖ f (pt A)) , rCancelₖ (suc n) (f (pt A)) - Iso.rightInv (fst main) = + Iso.sec (fst main) = ST.elim (λ _ → isSetPathImplicit) λ f → PT.rec (squash₂ _ _) (λ p → cong ∣_∣₂ (funExt λ x → cong (λ z → f x +ₖ z) (cong -ₖ_ p ∙ -0ₖ (suc n)) ∙ rUnitₖ (suc n) (f x))) (con-lem n (f (pt A))) - Iso.leftInv (fst main) = + Iso.ret (fst main) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) (funExt λ x → cong (fst f x +ₖ_) (cong -ₖ_ (snd f) ∙ -0ₖ (suc n)) @@ -286,13 +286,13 @@ fst (coHom⁰≅coHomRed⁰ G A) = isoToEquiv is Iso.inv is = ST.rec (isSet× squash₂ (is-set (snd G))) λ f → ∣ (λ x → AbGroupStr._-_ (snd G) (f x) (f (pt A))) , +InvR (snd G) (f (pt A)) ∣₂ , f (pt A) - Iso.rightInv is = ST.elim (λ _ → isSetPathImplicit) + Iso.sec is = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt λ x → sym (+Assoc (snd G) _ _ _) ∙∙ cong (AbGroupStr._+_ (snd G) (f x)) (+InvL (snd G) (f (pt A))) ∙∙ +IdR (snd G) (f x)) - Iso.leftInv is = + Iso.ret is = uncurry (ST.elim (λ _ → isSetΠ (λ _ → isOfHLevelPath 2 (isSet× squash₂ (is-set (snd G))) _ _)) @@ -350,12 +350,12 @@ fst (coHomEquiv n f) = isoToEquiv is is : Iso _ _ Iso.fun is = coHomFun n (Iso.fun f) Iso.inv is = coHomFun n (Iso.inv f) - Iso.rightInv is = + Iso.sec is = ST.elim (λ _ → isSetPathImplicit) - λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.leftInv f x)) - Iso.leftInv is = + λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.ret f x)) + Iso.ret is = ST.elim (λ _ → isSetPathImplicit) - λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.rightInv f x)) + λ g → cong ∣_∣₂ (funExt λ x → cong g (Iso.sec f x)) snd (coHomEquiv n f) = snd (coHomHom n (Iso.fun f)) coHomFun∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''} @@ -441,14 +441,14 @@ EM→-charac : ∀ {ℓ ℓ'} {A : Pointed ℓ} {G : AbGroup ℓ'} (n : ℕ) Iso.fun (EM→-charac {A = A} n) f = ((λ x → f x -ₖ f (pt A)) , rCancelₖ n (f (pt A))) , f (pt A) Iso.inv (EM→-charac n) (f , a) x = fst f x +ₖ a -Iso.rightInv (EM→-charac {A = A} n) ((f , p) , a) = +Iso.sec (EM→-charac {A = A} n) ((f , p) , a) = ΣPathP (→∙Homogeneous≡ (isHomogeneousEM _) (funExt (λ x → (λ i → (f x +ₖ a) -ₖ (cong (_+ₖ a) p ∙ lUnitₖ n a) i) ∙ sym (assocₖ n (f x) a (-ₖ a)) ∙ cong (f x +ₖ_) (rCancelₖ n a) ∙ rUnitₖ n (f x))) , cong (_+ₖ a) p ∙ lUnitₖ n a) -Iso.leftInv (EM→-charac {A = A} n) f = +Iso.ret (EM→-charac {A = A} n) f = funExt λ x → sym (assocₖ n (f x) (-ₖ f (pt A)) (f (pt A))) ∙∙ cong (f x +ₖ_) (lCancelₖ n (f (pt A))) ∙∙ rUnitₖ n (f x) diff --git a/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda index 4065a843fb..7e700e9a29 100644 --- a/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda +++ b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda @@ -145,7 +145,7 @@ module _ where inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n) inv (fst (suspMapIso (negsuc zero))) _ = 0ₕ∙ zero inv (fst (suspMapIso (negsuc (suc n)))) _ = tt* - rightInv (fst (suspMapIso (pos n) {A = A})) = + sec (fst (suspMapIso (pos n) {A = A})) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) (funExt λ x → cong (ΩEM+1→EM n) @@ -156,10 +156,10 @@ module _ where (cong sym (cong (EM→ΩEM+1 n) (snd f) ∙ EM→ΩEM+1-0ₖ n)) ∙ sym (rUnit _)) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) (fst f x))) - rightInv (fst (suspMapIso (negsuc zero))) tt* = refl - rightInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl - leftInv (fst (suspMapIso (pos n) {A = A})) = + ∙ Iso.ret (Iso-EM-ΩEM+1 n) (fst f x))) + sec (fst (suspMapIso (negsuc zero))) tt* = refl + sec (fst (suspMapIso (negsuc (suc n)))) tt* = refl + ret (fst (suspMapIso (pos n) {A = A})) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n)) (funExt λ { north → sym (snd f) @@ -172,7 +172,7 @@ module _ where ∙∙ cong (fst f) (toSusp A a) ∙∙ snd f))) (cong (fst f) (merid a)) - lem a f = Iso.rightInv (Iso-EM-ΩEM+1 n) _ + lem a f = Iso.sec (Iso-EM-ΩEM+1 n) _ ◁ λ i j → hcomp (λ k → λ { (i = i1) → fst f (merid a j) ; (j = i0) → snd f (~ i ∧ k) @@ -180,13 +180,13 @@ module _ where (sym (snd f)) (cong (fst f) (merid (pt A))) k i}) (fst f (compPath-filler (merid a) (sym (merid (pt A))) (~ i) j)) - leftInv (fst (suspMapIso (negsuc zero) {A = A})) = + ret (fst (suspMapIso (negsuc zero) {A = A})) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) (funExt (suspToPropElim (pt A) (λ _ → hLevelEM G 0 _ _) (sym (snd f))))) - leftInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl + ret (fst (suspMapIso (negsuc (suc n)))) tt* = refl snd (suspMapIso n) = suspMap n .snd satisfies-ES : ∀ {ℓ ℓ'} (G : AbGroup ℓ) → coHomTheory {ℓ'} (coHomRedℤ G) @@ -237,8 +237,8 @@ module _ where (Im (coHomHom∙ n (cfcod (fst f) , refl))) fun help (x , p) = x , To x p inv help (x , p) = x , From x p - rightInv help (x , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl - leftInv help (x , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl + sec help (x , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl + ret help (x , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl Exactness (satisfies-ES {ℓ} {ℓ'} G) {A = A} {B = B} f (negsuc n) = isoToPath help where @@ -247,8 +247,8 @@ module _ where (cfcod (fst f) , refl))) fun help (tt* , p) = tt* , ∣ tt* , refl ∣₁ inv help (tt* , p) = tt* , refl - rightInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl - leftInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl + sec help (tt* , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl + ret help (tt* , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl Dimension (satisfies-ES G) (pos zero) p = ⊥.rec (p refl) fst (Dimension (satisfies-ES G) (pos (suc n)) _) = 0ₕ∙ (suc n) snd (Dimension (satisfies-ES G) (pos (suc n)) _) = @@ -274,13 +274,13 @@ module _ where ; (inr x) → fst g x ; (push a i) → (snd f ∙ sym (snd g)) i}) , snd f ∣₂) - rightInv (fst main) = + sec (fst main) = uncurry (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) λ f g → ΣPathP ((cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)) , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))) - leftInv (fst main) = + ret (fst main) = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) (funExt λ { (inl x) → refl @@ -325,9 +325,9 @@ Wedge (satisfies-ES-gen G) (pos n) {I = I} satAC {A = A} = ; (inr x) → f (fst x) .fst (snd x) ; (push a i) → f a .snd (~ i)}) , refl - rightInv mainIso = ST.elim (λ _ → isSetPathImplicit) + sec mainIso = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt (λ i → ΣPathP (refl , (sym (rUnit (snd (f i))))))) - leftInv mainIso = ST.elim (λ _ → isSetPathImplicit) + ret mainIso = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ { (inl x) → sym (snd f) ; (inr x) → refl diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Connected.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Connected.agda index 05d173b327..eddd42a393 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Connected.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Connected.agda @@ -65,8 +65,8 @@ module _ {A : Type ℓ} (conA : isConnected 2 A) (G : AbGroup ℓ') where is : Iso _ _ Iso.fun is = G→H⁰ Iso.inv is = H⁰→G - Iso.rightInv is = H⁰→G→H⁰ - Iso.leftInv is = G→H⁰→G + Iso.sec is = H⁰→G→H⁰ + Iso.ret is = G→H⁰→G snd H⁰conn' = makeIsGroupHom λ _ _ → refl H⁰conn : AbGroupEquiv (coHomGr zero G A) G diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda index 047df48a83..1a2d85815e 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/KleinBottle.agda @@ -174,8 +174,8 @@ H¹K²→ℤ/2×ℤ/2 = ST.rec (is-set (snd (dirProdAb ℤ/2 ℤ/2))) ℤ/2×ℤ/2→H¹K²→ℤ/2×ℤ/2 : (x : fst (dirProdAb ℤ/2 ℤ/2)) → H¹K²→ℤ/2×ℤ/2 (ℤ/2×ℤ/2→H¹K² x) ≡ x ℤ/2×ℤ/2→H¹K²→ℤ/2×ℤ/2 (g₁ , g₂) = - ΣPathP ((Iso.leftInv (Iso-EM-ΩEM+1 0) g₁) - , Iso.leftInv (Iso-EM-ΩEM+1 0) g₂) + ΣPathP ((Iso.ret (Iso-EM-ΩEM+1 0) g₁) + , Iso.ret (Iso-EM-ΩEM+1 0) g₂) H¹K²→ℤ/2×ℤ/2→H¹K² : (x : _) → ℤ/2×ℤ/2→H¹K² (H¹K²→ℤ/2×ℤ/2 x) ≡ x @@ -183,8 +183,8 @@ H¹K²→ℤ/2×ℤ/2→H¹K² = ST.elim (λ _ → isSetPathImplicit) (ConnK².elim₁ (isConnectedEM 1) (λ _ → squash₂ _ _) embase λ l1 l2 sq → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM _ 1 _ _) refl - (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 0) l1)) - (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 0) l2))))) + (flipSquare (Iso.sec (Iso-EM-ΩEM+1 0) l1)) + (flipSquare (Iso.sec (Iso-EM-ΩEM+1 0) l2))))) ℤ/2×ℤ/2≅H¹[K²,ℤ/2] : AbGroupEquiv (dirProdAb ℤ/2 ℤ/2) (coHomGr 1 ℤ/2 KleinBottle) @@ -193,8 +193,8 @@ fst ℤ/2×ℤ/2≅H¹[K²,ℤ/2] = isoToEquiv is is : Iso _ _ Iso.fun is = ℤ/2×ℤ/2→H¹K² Iso.inv is = H¹K²→ℤ/2×ℤ/2 - Iso.rightInv is = H¹K²→ℤ/2×ℤ/2→H¹K² - Iso.leftInv is = ℤ/2×ℤ/2→H¹K²→ℤ/2×ℤ/2 + Iso.sec is = H¹K²→ℤ/2×ℤ/2→H¹K² + Iso.ret is = ℤ/2×ℤ/2→H¹K²→ℤ/2×ℤ/2 snd ℤ/2×ℤ/2≅H¹[K²,ℤ/2] = makeIsGroupHom λ x y → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM _ 1 _ _) refl @@ -284,11 +284,11 @@ H²K²→ℤ/2→H²K² = λ { point → refl ; (line1 i) → refl ; (line2 i) → refl - ; (square i j) k → Iso.leftInv Iso-Ω²K₂-ℤ/2 sq k i j})) + ; (square i j) k → Iso.ret Iso-Ω²K₂-ℤ/2 sq k i j})) ℤ/2→H²K²→ℤ/2 : (g : fst ℤ/2) → H²K²→ℤ/2 (ℤ/2→H²K² g) ≡ g ℤ/2→H²K²→ℤ/2 g = - H²K²→ℤ/2-rewrite (ℤ/2→Ω²K₂ g) ∙ (Iso.rightInv Iso-Ω²K₂-ℤ/2 g) + H²K²→ℤ/2-rewrite (ℤ/2→Ω²K₂ g) ∙ (Iso.sec Iso-Ω²K₂-ℤ/2 g) KleinFun-triv : ∀ {ℓ} {A : Type ℓ} {a : A} → KleinFun a refl refl refl ≡ λ _ → a KleinFun-triv = @@ -311,8 +311,8 @@ fst H²[K²,ℤ/2]≅ℤ/2 = isoToEquiv is is : Iso _ _ Iso.fun is = H²K²→ℤ/2 Iso.inv is = ℤ/2→H²K² - Iso.rightInv is = ℤ/2→H²K²→ℤ/2 - Iso.leftInv is = H²K²→ℤ/2→H²K² + Iso.sec is = ℤ/2→H²K²→ℤ/2 + Iso.ret is = H²K²→ℤ/2→H²K² snd H²[K²,ℤ/2]≅ℤ/2 = Isoℤ/2-morph (fst H²[K²,ℤ/2]≅ℤ/2) (0ₕ 2) (sym H²K²→ℤ/2-pres0) _+ₕ_ (-ₕ_) (funExt (ST.elim (λ _ → isSetPathImplicit) @@ -389,16 +389,16 @@ fst (H¹[K²,G]≅G×H¹[RP²,G] G) = isoToEquiv mainIso ST.rec (isSet× (is-set (snd G)) squash₂) λ f → (ΩEM+1→EM-gen 0 _ (cong f line2)) , ∣ F→ f ∣₂ Iso.inv mainIso = uncurry λ g → ST.map (F← g) - Iso.rightInv mainIso = uncurry λ g + Iso.sec mainIso = uncurry λ g → ST.elim (λ _ → isOfHLevelPath 2 (isSet× (is-set (snd G)) squash₂) _ _) - λ f → ΣPathP ((Iso.leftInv (Iso-EM-ΩEM+1-gen 0 (f point)) g) + λ f → ΣPathP ((Iso.ret (Iso-EM-ΩEM+1-gen 0 (f point)) g) , cong ∣_∣₂ (funExt (elimSetRP² (λ _ → hLevelEM G 1 _ _) refl λ i j → f (line i)))) - Iso.leftInv mainIso = ST.elim (λ _ → isSetPathImplicit) + Iso.ret mainIso = ST.elim (λ _ → isSetPathImplicit) λ f → cong ∣_∣₂ (funExt (elimSet (λ _ → hLevelEM G 1 _ _) refl (λ i j → f (line1 i)) - (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1-gen 0 (f point)) (cong f line2))))) + (flipSquare (Iso.sec (Iso-EM-ΩEM+1-gen 0 (f point)) (cong f line2))))) snd (H¹[K²,G]≅G×H¹[RP²,G] G) = makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 lem _ _) @@ -445,14 +445,14 @@ private (EM-raw'-trivElim G (suc n) (λ _ → isOfHLevelΠ (2 +ℕ n) λ _ → isOfHLevelPlus' {n = n} 2 squash₂) ∣_∣₂))) - Iso.rightInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) + Iso.sec (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) (uncurry (EM-raw'-elim G (2 +ℕ n) (λ _ → isOfHLevelΠ (3 +ℕ n) λ _ → isOfHLevelPlus' {n = suc (suc n)} 1 (squash₂ _ _)) (EM-raw'-trivElim G (suc n) (λ _ → isOfHLevelΠ (2 +ℕ n) λ _ → isOfHLevelPlus' {n = suc n} 1 (squash₂ _ _)) λ _ → refl))) - Iso.leftInv (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl + Iso.ret (H²K²-helperIso₁ G n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl H²K²-helperIso₂ : (G : AbGroup ℓ) (n : ℕ) → Iso ∥ (Σ[ p ∈ Ω (EM∙ G (2 +ℕ n)) .fst ] @@ -461,7 +461,7 @@ private p ≡ sym p)) ∥₂ Iso.fun (H²K²-helperIso₂ G n) = ST.map (H²K²-helperFun₁ G n) Iso.inv (H²K²-helperIso₂ G n) = ST.map (λ p → fst p , refl , sym (snd p)) - Iso.rightInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) λ {(p , r) + Iso.sec (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) λ {(p , r) → TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) (λ { P → cong ∣_∣₂ (main p P r)}) ((F p .fst))} @@ -473,7 +473,7 @@ private → H²K²-helperFun₁ G n (p , refl , sym r) ≡ (p , r) main = (J> λ r → (ΣPathP (refl , sym (rUnit _) ∙ λ i j k → rUnitₖ (suc (suc n)) (r j k) i))) - Iso.leftInv (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) + Iso.ret (H²K²-helperIso₂ G n) = ST.elim (λ _ → isSetPathImplicit) (uncurry λ p → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ ))) (λ P → uncurry λ q → TR.rec (isProp→isOfHLevelSuc n (isPropΠ (λ _ → squash₂ _ _ ))) (λ Q x → cong ∣_∣₂ (main p P q Q x)) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda index 370ab29351..7327b91185 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/RP2.agda @@ -140,7 +140,7 @@ H¹[RP²,ℤ/2]→ℤ/2 = ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 : (x : fst ℤ/2) → H¹[RP²,ℤ/2]→ℤ/2 (ℤ/2→H¹[RP²,ℤ/2] x) ≡ x -ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 = Iso.leftInv (Iso-EM-ΩEM+1 0) +ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 = Iso.ret (Iso-EM-ΩEM+1 0) H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] : (f : coHom 1 ℤ/2 RP²) → ℤ/2→H¹[RP²,ℤ/2] (H¹[RP²,ℤ/2]→ℤ/2 f) ≡ f @@ -153,7 +153,7 @@ H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] = λ l sq → cong ∣_∣₂ (funExt (elimSetRP² (λ _ → hLevelEM _ 1 _ _) refl - (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 0) l))))) + (flipSquare (Iso.sec (Iso-EM-ΩEM+1 0) l))))) H¹[RP²,ℤ/2]≅ℤ/2 : AbGroupEquiv (coHomGr 1 ℤ/2 RP²) ℤ/2 fst H¹[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is @@ -161,8 +161,8 @@ fst H¹[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is is : Iso _ _ Iso.fun is = H¹[RP²,ℤ/2]→ℤ/2 Iso.inv is = ℤ/2→H¹[RP²,ℤ/2] - Iso.rightInv is = ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 - Iso.leftInv is = H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] + Iso.sec is = ℤ/2→H¹[RP²,ℤ/2]→ℤ/2 + Iso.ret is = H¹[RP²,ℤ/2]→ℤ/2→H¹[RP²,ℤ/2] snd H¹[RP²,ℤ/2]≅ℤ/2 = isGroupHomInv ((invEquiv (fst H¹[RP²,ℤ/2]≅ℤ/2)) , makeIsGroupHom λ x y → cong ∣_∣₂ @@ -197,7 +197,7 @@ H²[RP²,ℤ/2]→ℤ/2-Id q = cong (Iso.fun Iso-Ω²K₂-ℤ/2) lem → H²[RP²,ℤ/2]→ℤ/2 (ℤ/2→H²[RP²,ℤ/2] x) ≡ x ℤ/2→H²[RP²,ℤ/2]→ℤ/2 x = H²[RP²,ℤ/2]→ℤ/2-Id (Iso.inv Iso-Ω²K₂-ℤ/2 x) - ∙ Iso.rightInv Iso-Ω²K₂-ℤ/2 x + ∙ Iso.sec Iso-Ω²K₂-ℤ/2 x H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] : (x : coHom 2 ℤ/2 RP²) → ℤ/2→H²[RP²,ℤ/2] (H²[RP²,ℤ/2]→ℤ/2 x) ≡ x @@ -210,7 +210,7 @@ H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] = λ sq → cong (ℤ/2→H²[RP²,ℤ/2]) (H²[RP²,ℤ/2]→ℤ/2-Id sq) ∙ cong ∣_∣₂ (cong (RP²Fun (snd (EM∙ ℤ/2 2)) refl) - (Iso.leftInv Iso-Ω²K₂-ℤ/2 sq))) + (Iso.ret Iso-Ω²K₂-ℤ/2 sq))) H²[RP²,ℤ/2]≅ℤ/2 : AbGroupEquiv (coHomGr 2 ℤ/2 RP²) ℤ/2 fst H²[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is @@ -218,8 +218,8 @@ fst H²[RP²,ℤ/2]≅ℤ/2 = isoToEquiv is is : Iso _ _ Iso.fun is = H²[RP²,ℤ/2]→ℤ/2 Iso.inv is = ℤ/2→H²[RP²,ℤ/2] - Iso.rightInv is = ℤ/2→H²[RP²,ℤ/2]→ℤ/2 - Iso.leftInv is = H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] + Iso.sec is = ℤ/2→H²[RP²,ℤ/2]→ℤ/2 + Iso.ret is = H²[RP²,ℤ/2]→ℤ/2→H²[RP²,ℤ/2] snd H²[RP²,ℤ/2]≅ℤ/2 = Isoℤ/2-morph (fst H²[RP²,ℤ/2]≅ℤ/2) _ (sym (H²[RP²,ℤ/2]→ℤ/2-Id refl) @@ -296,16 +296,16 @@ module _ {ℓ : Level} (G : AbGroup ℓ) where is : Iso _ _ Iso.fun is = H¹[RP²,G]→G[2] Iso.inv is = G[2]→H¹[RP²,G] - Iso.rightInv is (g , p) = + Iso.sec is (g , p) = Σ≡Prop (λ _ → is-set (snd G) _ _) - (Iso.leftInv (Iso-EM-ΩEM+1 0) g) - Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit) + (Iso.ret (Iso-EM-ΩEM+1 0) g) + Iso.ret is = ST.elim (λ _ → isSetPathImplicit) (RP²Conn.elim₁ (isConnectedEM 1) (λ _ → squash₂ _ _) embase λ p q → cong ∣_∣₂ (funExt (elimSetRP² (λ _ → emsquash _ _) refl - (flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 {G = G} 0) p))))) + (flipSquare (Iso.sec (Iso-EM-ΩEM+1 {G = G} 0) p))))) snd G[2]≅H¹[RP²,G] = makeIsGroupHom λ x y → cong ∣_∣₂ (funExt (elimSetRP² (λ _ → emsquash _ _) refl @@ -350,8 +350,8 @@ module _ (G : AbGroup ℓ) where (λ _ → isOfHLevelΠ (suc (suc n)) λ _ → isOfHLevelPlus' {n = n} 2 squash₂) ∣_∣₂))) Iso.inv (killFirstCompIsoGen n) = ST.map (0ₖ (2 +ℕ n) ,_) - Iso.rightInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl - Iso.leftInv (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) + Iso.sec (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) λ _ → refl + Iso.ret (killFirstCompIsoGen n) = ST.elim (λ _ → isSetPathImplicit) (uncurry (TR.elim (λ _ → isProp→isOfHLevelSuc (3 +ℕ n) (isPropΠ (λ _ → squash₂ _ _))) (EM-raw'-trivElim G (suc n) (λ _ → isProp→isOfHLevelSuc (suc n) @@ -435,7 +435,7 @@ module _ (G : AbGroup ℓ) where , cong (snd G ._+_ g) (+IdR (snd G) _) ∙ sym (+IdR (snd G) (snd G ._+_ g g)) ∙ cong₂ (snd G ._+_) - (sym (Iso.leftInv (Iso-EM-ΩEM+1 0) _) + (sym (Iso.ret (Iso-EM-ΩEM+1 0) _) ∙ cong (ΩEM+1→EM 0) (emloop-comp _ g g)) (sym (+InvR (snd G) (ΩEM+1→EM 0 q))) ∙ +Assoc (snd G) _ _ _ ∣₁) @@ -464,11 +464,11 @@ module _ (G : AbGroup ℓ) where ∙ (sym (+Assoc (snd G) _ _ _) ∙ cong (_+_ (snd G) b) (+InvL (snd G) a)) ∙ +IdR (snd G) b))))) - Iso.rightInv H²RP²-Iso₃ = SQ.elimProp (λ _ → squash/ _ _) - λ a → cong [_] (Iso.leftInv (Iso-EM-ΩEM+1 0) a) - Iso.leftInv H²RP²-Iso₃ = ST.elim (λ _ → isSetPathImplicit) + Iso.sec H²RP²-Iso₃ = SQ.elimProp (λ _ → squash/ _ _) + λ a → cong [_] (Iso.ret (Iso-EM-ΩEM+1 0) a) + Iso.ret H²RP²-Iso₃ = ST.elim (λ _ → isSetPathImplicit) (uncurry (EM1.elimProp (AbGroup→Group G) (λ _ → isPropΠ λ _ → squash₂ _ _) - λ p → cong ∣_∣₂ (ΣPathP (refl , (Iso.rightInv (Iso-EM-ΩEM+1 0) p))))) + λ p → cong ∣_∣₂ (ΣPathP (refl , (Iso.sec (Iso-EM-ΩEM+1 0) p))))) H²[RP²,G]≅G/2 : AbGroupEquiv (coHomGr 2 G RP²) (G /^ 2) fst H²[RP²,G]≅G/2 = isoToEquiv is diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda index 8a1d36f8df..64932ebcb4 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/RPinf.agda @@ -214,8 +214,8 @@ RP→Charac₀ : Iso (EM ℤ/2 1 → ℤ/2 .fst) (ℤ/2 .fst) Iso.fun RP→Charac₀ f = f embase Iso.inv RP→Charac₀ a = λ _ → a -Iso.rightInv RP→Charac₀ a = refl -Iso.leftInv RP→Charac₀ f = +Iso.sec RP→Charac₀ a = refl +Iso.ret RP→Charac₀ f = funExt (EM→Prop _ 0 (λ _ → is-set (snd ℤ/2Ring) _ _) refl) RP→EM-ℤ/2-CharacIso : (n : ℕ) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda index 315fb97694..7ac1bd51de 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda @@ -109,12 +109,12 @@ module _ (G : AbGroup ℓ) where is : Iso _ _ Iso.fun is = H¹S¹→G Iso.inv is = G→H¹S¹ - Iso.rightInv is = Iso.leftInv (Iso-EM-ΩEM+1 0) - Iso.leftInv is = + Iso.sec is = Iso.ret (Iso-EM-ΩEM+1 0) + Iso.ret is = ST.elim (λ _ → isSetPathImplicit) (S¹-connElim (isConnectedEM 1) (λ _ → squash₂ _ _) embase - λ p → cong ∣_∣₂ (cong (S¹fun embase) (Iso.rightInv (Iso-EM-ΩEM+1 0) p))) + λ p → cong ∣_∣₂ (cong (S¹fun embase) (Iso.sec (Iso-EM-ΩEM+1 0) p))) snd H¹[S¹,G]≅G = isGroupHomInv ((invEquiv (fst H¹[S¹,G]≅G)) , makeIsGroupHom λ x y → cong ∣_∣₂ @@ -143,7 +143,7 @@ module _ (G : AbGroup ℓ) where is : Iso _ _ Iso.fun is = HⁿSⁿ↑ n Iso.inv is = HⁿSⁿ↓ n - Iso.rightInv is = + Iso.sec is = ST.elim (λ _ → isSetPathImplicit) (Sⁿ-connElim n (isConnectedSubtr 2 (suc n) (subst (λ x → isConnected x (EM G (suc (suc n)))) @@ -159,12 +159,12 @@ module _ (G : AbGroup ℓ) where (merid x) (sym (merid (ptSn (suc n)))) ∙ cong (p x ∙_) (cong sym q) ∙ sym (rUnit (p x))) - ∙ Iso.rightInv (Iso-EM-ΩEM+1 (suc n)) (p x))))) + ∙ Iso.sec (Iso-EM-ΩEM+1 (suc n)) (p x))))) (isConnectedPath (suc n) (isConnectedPath (suc (suc n)) (isConnectedEM (suc (suc n))) _ _) (p (ptSn _)) refl .fst)) - Iso.leftInv is = ST.elim (λ _ → isSetPathImplicit) + Iso.ret is = ST.elim (λ _ → isSetPathImplicit) λ f → TR.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) (λ q → cong ∣_∣₂ (funExt λ x → cong (ΩEM+1→EM (suc n)) @@ -173,7 +173,7 @@ module _ (G : AbGroup ℓ) where (cong sym (cong (EM→ΩEM+1 (suc n)) q ∙ EM→ΩEM+1-0ₖ (suc n))) ∙ sym (rUnit _)) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) (f x))) + ∙ Iso.ret (Iso-EM-ΩEM+1 (suc n)) (f x))) (isConnectedPath (suc n) (isConnectedEM (suc n)) (f (ptSn (suc n))) (0ₖ (suc n)) .fst) @@ -413,11 +413,11 @@ gen-HⁿSⁿ-raw↦1 R (suc (suc n)) = (merid x) (sym (merid (ptSn (suc n))))) ∙ ΩEM+1→EM-hom (suc n) _ _) ∙ cong₂ _+ₖ_ - (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) + (Iso.ret (Iso-EM-ΩEM+1 (suc n)) (gen-HⁿSⁿ-raw R (suc n) .fst x)) (((λ i → ΩEM+1→EM-sym (suc n) (EM→ΩEM+1 (suc n) (snd (gen-HⁿSⁿ-raw R (suc n)) i)) i) - ∙ cong -ₖ_ (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) (0ₖ (suc n))) + ∙ cong -ₖ_ (Iso.ret (Iso-EM-ΩEM+1 (suc n)) (0ₖ (suc n))) ∙ -0ₖ (suc n))) ∙ rUnitₖ (suc n) _)) ∙ gen-HⁿSⁿ-raw↦1 R (suc n) @@ -457,7 +457,7 @@ HⁿSⁿ-raw≃G-inv-isInv R (suc (suc n)) r = (isHomogeneousEM _) (funExt λ z → cong (ΩEM+1→EM (suc n)) (lem z) - ∙ Iso-EM-ΩEM+1 (suc n) .Iso.leftInv (subst (EM (Ring→AbGroup R)) + ∙ Iso-EM-ΩEM+1 (suc n) .Iso.ret (subst (EM (Ring→AbGroup R)) (+'-comm (suc n) 0) (_⌣ₖ_ {m = 0} (fst (gen-HⁿSⁿ-raw R (suc n)) z) r))))) ∙ HⁿSⁿ-raw≃G-inv-isInv R (suc n) r diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Torus.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Torus.agda index 6abcaf3d9c..1854eadb5c 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Torus.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Torus.agda @@ -156,7 +156,7 @@ H¹[T²,G]≅G×G G = λ f → ∣ (λ x → f (x , base)) ∣₂ , ∣ (λ x → f (base , x)) ∣₂ Iso.inv typIso = uncurry (ST.rec2 squash₂ λ f g → ∣ (λ x → f (fst x) +1 g (snd x)) ∣₂) - Iso.rightInv typIso = + Iso.sec typIso = uncurry (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) (S¹-connElim (isConnectedEM {G' = G} 1) (λ _ → isPropΠ λ _ → isSet× squash₂ squash₂ _ _) @@ -166,7 +166,7 @@ H¹[T²,G]≅G×G G = (0ₖ {G = G} 1) λ q i → ∣ (λ l → rUnitₖ {G = G} 1 (S¹fun (0ₖ {G = G} 1) p l) i) ∣₂ , ∣ S¹fun (0ₖ {G = G} 1) q ∣₂)) - Iso.leftInv typIso = coHomPointedElimT² {G = G} 0 (λ _ → squash₂ _ _) + Iso.ret typIso = coHomPointedElimT² {G = G} 0 (λ _ → squash₂ _ _) λ p q r → cong ∣_∣₂ (funExt (uncurry (S¹elim _ (λ _ → refl) (funExt (toPropElim (λ _ → isOfHLevelPathP' 1 (hLevelEM G 1 _ _) _ _ ) diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda index 25d2fe03b1..09d3a3ab8e 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Wedge.agda @@ -64,7 +64,7 @@ module _ {A : Pointed ℓ} {B : Pointed ℓ'} (G : AbGroup ℓ) where λ f → ∣ f ∘ inl ∣₂ , ∣ f ∘ inr ∣₂ Iso.inv (Hⁿ⋁-Iso n) = uncurry (ST.rec2 squash₂ λ f g → ∣ Hⁿ-⋁→Hⁿ× n f g ∣₂) - Iso.rightInv (Hⁿ⋁-Iso n) = + Iso.sec (Hⁿ⋁-Iso n) = uncurry (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _) λ f g @@ -80,7 +80,7 @@ module _ {A : Pointed ℓ} {B : Pointed ℓ'} (G : AbGroup ℓ) where ∙ rUnitₖ (suc n) (g x))) (isConnectedPath (suc n) (isConnectedEM (suc n)) (g (pt B)) (0ₖ (suc n)) .fst))) - Iso.leftInv (Hⁿ⋁-Iso n) = + Iso.ret (Hⁿ⋁-Iso n) = ST.elim (λ _ → isSetPathImplicit) λ f → Trunc.rec (isProp→isOfHLevelSuc n (squash₂ _ _)) (λ p → cong ∣_∣₂ diff --git a/Cubical/Cohomology/EilenbergMacLane/Gysin.agda b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda index c86e76099b..db98edee7b 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Gysin.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda @@ -107,8 +107,8 @@ module ⌣Eq (R' : CommRing ℓ'') where -ₖ^-iso : ∀ {ℓ} {G : AbGroup ℓ} {k : ℕ} (n m : ℕ) → Iso (EM G k) (EM G k) Iso.fun (-ₖ^-iso n m) = -ₖ^[ n · m ] Iso.inv (-ₖ^-iso n m) = -ₖ^[ n · m ] - Iso.rightInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ - Iso.leftInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ + Iso.sec (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ + Iso.ret (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ g-cute' : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (n +' i) g-cute' n i = @@ -185,16 +185,16 @@ module ⌣Eq (R' : CommRing ℓ'') where , flipSquare ((λ j → EM→ΩEM+1-gen (i + n) (snd f j) (snd st j)) ▷ (EM→ΩEM+1-gen-0ₖ (i + n) _ ∙ EM→ΩEM+1-0ₖ (i + n)))) - Iso.rightInv (ΩFunIso n i f) st = + Iso.sec (ΩFunIso n i f) st = →∙Homogeneous≡ (isHomogeneousEM _) (funExt λ x - → Iso.leftInv (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) (st .fst x)) - Iso.leftInv (ΩFunIso n i f) st = + → Iso.ret (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) (st .fst x)) + Iso.ret (ΩFunIso n i f) st = →∙HomogeneousSquare (isHomogeneousEM _) refl refl (Iso.inv (ΩFunIso n i f) (Iso.fun (ΩFunIso n i f) st)) st (cong funExt (funExt - λ x → Iso.rightInv + λ x → Iso.sec (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) λ i → st i .fst x)) g-cute-ind : (n i : ℕ) @@ -209,7 +209,7 @@ module ⌣Eq (R' : CommRing ℓ'') where (λ i → transportRefl (_⌣ₖ_ {n = 1} {m = 0} (EM→ΩEM+1 0 x i) (gen-HⁿSⁿ-raw R zero .fst y)) j)) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 0) + ∙ Iso.ret (Iso-EM-ΩEM+1 0) (_⌣ₖ_ {n = 0} {m = 0} x (gen-HⁿSⁿ-raw R zero .fst y)))) g-cute-ind zero (suc i) = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) @@ -224,7 +224,7 @@ module ⌣Eq (R' : CommRing ℓ'') where (EM→ΩEM+1 (suc i) (_⌣ₖ_ {n = suc i} {m = zero} x (gen-HⁿSⁿ-raw R zero .fst y)) k))) ∙∙ cong (subst EMR (λ i₁ → suc (+-zero i (~ i₁)))) - (Iso.leftInv (Iso-EM-ΩEM+1 (suc i)) _))) + (Iso.ret (Iso-EM-ΩEM+1 (suc i)) _))) g-cute-ind (suc n) zero = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) (funExt λ y → transportRefl _ @@ -243,7 +243,7 @@ module ⌣Eq (R' : CommRing ℓ'') where (EM→ΩEM+1 (suc n) (x ⌣[ R , 0 , (suc n) ]ₖ gen-HⁿSⁿ-raw R (suc n) .fst y))) ∙ transportRefl _) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) _)) + ∙ Iso.ret (Iso-EM-ΩEM+1 (suc n)) _)) g-cute-ind (suc n) (suc i) = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) (funExt λ y @@ -256,7 +256,7 @@ module ⌣Eq (R' : CommRing ℓ'') where j (EM→ΩEM+1 (suc (suc (i + n))) (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y) k))))) ∙ cong (subst EMR (λ i₁ → suc (+-suc i n (~ i₁)))) - (Iso.leftInv (Iso-EM-ΩEM+1 (suc i +' suc n)) + (Iso.ret (Iso-EM-ΩEM+1 (suc i +' suc n)) (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y)))) g-ind-main : (n i : ℕ) @@ -285,9 +285,9 @@ module ⌣Eq (R' : CommRing ℓ'') where ≡ myEq .fst help = funExt (λ p → sym - (Iso.leftInv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) _ + (Iso.ret (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) _ ∙ cong (cong (g-cute n (suc i))) - (Iso.rightInv (Iso-EM-ΩEM+1 i) _))) + (Iso.sec (Iso-EM-ΩEM+1 i) _))) ∙ sym (cong (λ f → Iso.inv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) ∘ f ∘ ΩEM+1→EM i) @@ -422,8 +422,8 @@ module preThom → Iso (fst B → EMR i) ((b : fst B) → Q b →∙ EMR∙ (i +' n)) Iso.fun (pre-ϕIso i) = pre-ϕ i Iso.inv (pre-ϕIso i) r b = invEq (g-equiv i b) (r b) - Iso.rightInv (pre-ϕIso i) t j b = secEq (g-equiv i b) (t b) j - Iso.leftInv (pre-ϕIso i) t j b = retEq (g-equiv i b) (t b) j + Iso.sec (pre-ϕIso i) t j b = secEq (g-equiv i b) (t b) j + Iso.ret (pre-ϕIso i) t j b = retEq (g-equiv i b) (t b) j pre-ϕ-pres+ : (i : ℕ) → (f g : fst B → EMR i) → pre-ϕ i (λ b → f b +ₖ g b) ≡ λ b → pre-ϕ i f b +ₖ∙ pre-ϕ i g b @@ -531,10 +531,10 @@ module Thom (B : Pointed ℓ) Iso.fun (EP-contr c) (inr x) = x Iso.fun (EP-contr c) (push a i) = πE (isContr→isProp c (* , P*) a i) Iso.inv (EP-contr c) = inr - Iso.rightInv (EP-contr c) = λ _ → refl - Iso.leftInv (EP-contr c) (inl x) = sym (push (* , P*)) - Iso.leftInv (EP-contr c) (inr x) = refl - Iso.leftInv (EP-contr c) (push a i) j = + Iso.sec (EP-contr c) = λ _ → refl + Iso.ret (EP-contr c) (inl x) = sym (push (* , P*)) + Iso.ret (EP-contr c) (inr x) = refl + Iso.ret (EP-contr c) (push a i) j = hcomp (λ k → λ {(i = i0) → push (* , P*) (~ j) ; (i = i1) → push a (~ j ∨ k) ; (j = i0) → inr (πE (isContr→isProp c (* , P*) a i)) @@ -576,15 +576,15 @@ module Thom (B : Pointed ℓ) Iso-EP-FP : Iso EP FP Iso.fun Iso-EP-FP = EP→FP Iso.inv Iso-EP-FP = FP→EP - Iso.rightInv Iso-EP-FP (inl x) = refl - Iso.rightInv Iso-EP-FP (inr (x , north)) = push x - Iso.rightInv Iso-EP-FP (inr (x , south)) = refl - Iso.rightInv Iso-EP-FP (inr (x , merid a i)) j = + Iso.sec Iso-EP-FP (inl x) = refl + Iso.sec Iso-EP-FP (inr (x , north)) = push x + Iso.sec Iso-EP-FP (inr (x , south)) = refl + Iso.sec Iso-EP-FP (inr (x , merid a i)) j = compPath-filler' (push x) (λ j₁ → inr (x , merid a j₁)) (~ j) i - Iso.rightInv Iso-EP-FP (push a i) j = push a (i ∧ j) - Iso.leftInv Iso-EP-FP (inl x) = refl - Iso.leftInv Iso-EP-FP (inr x) = refl - Iso.leftInv Iso-EP-FP (push (b , p) i) j = + Iso.sec Iso-EP-FP (push a i) j = push a (i ∧ j) + Iso.ret Iso-EP-FP (inl x) = refl + Iso.ret Iso-EP-FP (inr x) = refl + Iso.ret Iso-EP-FP (push (b , p) i) j = (cong-∙ FP→EP (push b) (λ j → inr (b , merid p j)) ∙ sym (lUnit (push (b , p)))) j i @@ -605,8 +605,8 @@ module Thom (B : Pointed ℓ) fst (Iso.inv (mapIso isHom) r) (inr (b , p)) = r b .fst p fst (Iso.inv (mapIso isHom) r) (push a i) = r a .snd (~ i) snd (Iso.inv (mapIso isHom) r) = r (pt B) .snd - Iso.rightInv (mapIso isHom) r = funExt λ b → →∙Homogeneous≡ isHom refl - Iso.leftInv (mapIso isHom) r = + Iso.sec (mapIso isHom) r = funExt λ b → →∙Homogeneous≡ isHom refl + Iso.ret (mapIso isHom) r = →∙Homogeneous≡ isHom (funExt λ { (inl x) → sym (snd r) ∙ cong (fst r) (sym (push (pt B))) ; (inr x) → refl @@ -655,7 +655,7 @@ module Thom (B : Pointed ℓ) ι-pres+ k = morphLemmas.isMorphInv _+ₖ∙_ (λ f g b → f b +ₖ∙ g b) (Iso.inv (ι k)) (ι⁻-pres+ k) (Iso.fun (ι k)) - (Iso.leftInv (ι k)) (Iso.rightInv (ι k)) + (Iso.ret (ι k)) (Iso.sec (ι k)) -- We combine it with the generalised thom iso, in order to get the -- usual Thom isomorphism @@ -823,10 +823,10 @@ module Thom (B : Pointed ℓ) (rUnit _ ∙∙ sym (Square→compPath ((cong (funExt⁻ (cong fst r)) (push (* , P*))) ▷ λ i j → r j .snd i)) ∙∙ sym (rUnit _)))) - (Iso.leftInv (Iso-EM-ΩEM+1 i) (f (x , p)))) + (Iso.ret (Iso-EM-ΩEM+1 i) (f (x , p)))) ∙ cong₂ _+ₖ_ (cong₂ _+ₖ_ (cong (ΩEM+1→EM i) (sym (EM→ΩEM+1-sym i (f (* , P*)))) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 i) (-ₖ (f (* , P*)))) refl + ∙ Iso.ret (Iso-EM-ΩEM+1 i) (-ₖ (f (* , P*)))) refl ∙ commₖ i (-ₖ f (* , P*)) (f (x , p))) refl ∙ sym (assocₖ i (f (x , p)) (-ₖ (f (* , P*))) (f (* , P*))) @@ -874,7 +874,7 @@ module Thom (B : Pointed ℓ) (sym (snd f) ∙ cong (fst f) (sym (push (* , P*)))) (sym (p (fst a))) main a f p = - flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 i) (pth a f p) + flipSquare (Iso.sec (Iso-EM-ΩEM+1 i) (pth a f p) ◁ λ j i → doubleCompPath-filler (sym (snd f) ∙ cong (fst f) (sym (push (* , P*)))) (cong (fst f) (push a)) diff --git a/Cubical/Cohomology/EilenbergMacLane/MayerVietoris.agda b/Cubical/Cohomology/EilenbergMacLane/MayerVietoris.agda index d7d865f3d2..91c2d1eeb2 100644 --- a/Cubical/Cohomology/EilenbergMacLane/MayerVietoris.agda +++ b/Cubical/Cohomology/EilenbergMacLane/MayerVietoris.agda @@ -141,7 +141,7 @@ module MV {ℓ ℓ' ℓ'' ℓ'''} (G : AbGroup ℓ''') where help : Square (EM→ΩEM+1 n (F c)) (cong a (push c)) (sym (l (f c))) (sym (r (g c))) - help = Iso.rightInv (Iso-EM-ΩEM+1 n) _ + help = Iso.sec (Iso-EM-ΩEM+1 n) _ ◁ symP (doubleCompPath-filler (sym (l (f c))) (cong a (push c)) (r (g c))) @@ -211,7 +211,7 @@ module MV {ℓ ℓ' ℓ'' ℓ'''} (G : AbGroup ℓ''') , cong ∣_∣₂ (funExt λ c → distrHelper n (λ i₁ → p i₁ (inl (f c))) (λ i₁ → p i₁ (inr (g c))) ∙ cong (ΩEM+1→EM n) (help h p c) - ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) (h c))) + ∙ Iso.ret (Iso-EM-ΩEM+1 n) (h c))) (Iso.fun (PathIdTrunc₀Iso) p) where help : (h : _) (p : d-pre n h ≡ (λ _ → 0ₖ (suc n))) (c : C) diff --git a/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda b/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda index e006c8739f..f3fea1fb3a 100644 --- a/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda +++ b/Cubical/Cohomology/EilenbergMacLane/RingStructure.agda @@ -108,8 +108,8 @@ module CohomologyRing-Equiv is : Iso (coHom n R-ab X) (coHom n R-ab Y) fun is = ST.rec squash₂ (λ f → ∣ (λ y → f (inv e y)) ∣₂) inv is = ST.rec squash₂ (λ g → ∣ (λ x → g (fun e x)) ∣₂) - rightInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ f → cong ∣_∣₂ (funExt (λ y → cong f (rightInv e y)))) - leftInv is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ g → cong ∣_∣₂ (funExt (λ x → cong g (leftInv e x)))) + sec is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ f → cong ∣_∣₂ (funExt (λ y → cong f (sec e y)))) + ret is = ST.elim (λ _ → isProp→isSet (squash₂ _ _)) (λ g → cong ∣_∣₂ (funExt (λ x → cong g (ret e x)))) snd (coHomGr-Iso {n}) = makeIsGroupHom (ST.elim (λ _ → isProp→isSet λ u v i y → squash₂ _ _ (u y) (v y) i) (λ f → ST.elim (λ _ → isProp→isSet (squash₂ _ _)) @@ -140,13 +140,13 @@ module CohomologyRing-Equiv e-sect : (y : H* R Y) → H*-X→H*-Y (H*-Y→H*-X y) ≡ y e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*Y _ _) refl - (λ m a → cong (base m) (rightInv (fst coHomGr-Iso) a)) + (λ m a → cong (base m) (sec (fst coHomGr-Iso) a)) (λ {U V} ind-U ind-V → cong₂ _+H*Y_ ind-U ind-V) e-retr : (x : H* R X) → H*-Y→H*-X (H*-X→H*-Y x) ≡ x e-retr = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH*X _ _) refl - (λ n a → cong (base n) (leftInv (fst coHomGr-Iso) a)) + (λ n a → cong (base n) (ret (fst coHomGr-Iso) a)) (λ {U V} ind-U ind-V → cong₂ _+H*X_ ind-U ind-V) H*-X→H*-Y-pres1 : H*-X→H*-Y 1H*X ≡ 1H*Y @@ -181,7 +181,7 @@ module _ is : Iso (H* R X) (H* R Y) fun is = H*-X→H*-Y inv is = H*-Y→H*-X - rightInv is = e-sect - leftInv is = e-retr + sec is = e-sect + ret is = e-retr snd CohomologyRing-Equiv = makeIsRingHom H*-X→H*-Y-pres1 H*-X→H*-Y-pres+ H*-X→H*-Y-pres· diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda index 3c786f0f50..e2cb93f229 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/KleinBottle.agda @@ -544,7 +544,7 @@ module _ where β²↦0 = cong H²K²→ℤ/2 cupIdΒ ∙ ℤ/2→H²K²→ℤ/2 0 where ℤ/2→Ω²K₂-refl : ℤ/2→Ω²K₂ 0 ≡ refl - ℤ/2→Ω²K₂-refl = Iso.leftInv Iso-Ω²K₂-ℤ/2 refl + ℤ/2→Ω²K₂-refl = Iso.ret Iso-Ω²K₂-ℤ/2 refl cupIdΒ : _⌣_ {G'' = ℤ/2Ring} {n = 1} {m = 1} K²gen.β K²gen.β ≡ ∣ KleinFun (0ₖ 2) refl refl (ℤ/2→Ω²K₂ 0) ∣₂ @@ -891,7 +891,7 @@ fst ℤ/2[X,Y]/≅H*KleinBottle = isoToEquiv is is : Iso _ _ fun is = ℤ/2[X,Y]/I→H*Klein .fst inv is = H*Klein→ℤ/2[X,Y]/I - rightInv is = DS-Ind-Prop.f _ _ _ _ + sec is = DS-Ind-Prop.f _ _ _ _ (λ _ → trunc _ _) refl (λ { zero a → lem₀ a _ refl @@ -1015,7 +1015,7 @@ fst ℤ/2[X,Y]/≅H*KleinBottle = isoToEquiv is ∙∙ cong (invEq (H²[K²,ℤ/2]≅ℤ/2* .fst)) (p ∙ sym α²↦1') ∙∙ retEq (H²[K²,ℤ/2]≅ℤ/2* .fst) α⌣α - leftInv is = + ret is = SQ.elimProp (λ _ → squash/ _ _) (DS-Ind-Prop.f _ _ _ _ diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda index 1e410fc14a..c6a91c95fd 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2.agda @@ -85,7 +85,7 @@ private γ↦1'' p q = H²[RP²,ℤ/2]→ℤ/2-Id p ∙ cong (Iso.fun Iso-Ω²K₂-ℤ/2) q - ∙ Iso.rightInv Iso-Ω²K₂-ℤ/2 1 + ∙ Iso.sec Iso-Ω²K₂-ℤ/2 1 cp : EM ℤ/2 1 → EM ℤ/2 1 → EM (ℤ/2 ⨂ ℤ/2) 2 cp = _⌣ₖ⊗_ {G' = ℤ/2} {H' = ℤ/2} {n = 1} {m = 1} diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda index b4263d4dbb..d8aaab1504 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/RP2wedgeS1.agda @@ -138,7 +138,7 @@ private γ↦1' p q = H²[RP²,ℤ/2]→ℤ/2-Id p ∙ cong (Iso.fun Iso-Ω²K₂-ℤ/2) q - ∙ Iso.rightInv Iso-Ω²K₂-ℤ/2 1 + ∙ Iso.sec Iso-Ω²K₂-ℤ/2 1 private cp : EM ℤ/2 1 → EM ℤ/2 1 → EM (ℤ/2 ⨂ ℤ/2) 2 @@ -359,22 +359,22 @@ module Equiv-RP²∨S¹-Properties ϕ₀str = snd e₀ ϕ₀⁻¹ = inv (fst e₀) ϕ₀⁻¹str = snd (invGroupIso e₀) - ϕ₀-sect = rightInv (fst e₀) - ϕ₀-retr = leftInv (fst e₀) + ϕ₀-sect = sec (fst e₀) + ϕ₀-retr = ret (fst e₀) ϕ₁ = fun (fst e₁) ϕ₁str = snd e₁ ϕ₁⁻¹ = inv (fst e₁) ϕ₁⁻¹str = snd (invGroupIso e₁) - ϕ₁-sect = rightInv (fst e₁) - ϕ₁-retr = leftInv (fst e₁) + ϕ₁-sect = sec (fst e₁) + ϕ₁-retr = ret (fst e₁) ϕ₂ = fun (fst e₂) ϕ₂str = snd e₂ ϕ₂⁻¹ = inv (fst e₂) ϕ₂⁻¹str = snd (invGroupIso e₂) - ϕ₂-sect = rightInv (fst e₂) - ϕ₂-retr = leftInv (fst e₂) + ϕ₂-sect = sec (fst e₂) + ϕ₂-retr = ret (fst e₂) ϕ₁left : fst ℤ/2 → coHom 1 ℤ/2 RP²∨S¹ ϕ₁left a = ϕ₁ (a , 0ℤ/2) @@ -793,6 +793,6 @@ module _ where is : Iso _ _ fun is = ℤ/2[X,Y]/→H*R-RP²∨S¹ .fst inv is = H*-RP²∨S¹→ℤ/2[x,y]/ - rightInv is = e-sect - leftInv is = e-retr + sec is = e-sect + ret is = e-retr snd RP²∨S¹-CohomologyRing = ℤ/2[X,Y]/→H*R-RP²∨S¹ .snd diff --git a/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda index bcac931ac9..3c9c3e003e 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Rings/Sn.agda @@ -123,7 +123,7 @@ module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where λ p → cong (H¹S¹→G (Ring→AbGroup G)) (cong (_⌣_ {G'' = G} {n = 0} {1} ∣ (λ _ → g) ∣₂) (cong (∣_∣₂ ∘ S¹Fun embase) - (sym (Iso.rightInv (Iso-EM-ΩEM+1 0) p)))) + (sym (Iso.sec (Iso-EM-ΩEM+1 0) p)))) ∙∙ help (ΩEM+1→EM 0 p) ∙∙ cong (RingStr._·_ (snd G) g) (λ _ → ΩEM+1→EM 0 p)) where @@ -132,7 +132,7 @@ module _ {ℓ : Level} (G : CommRing ℓ) (n : ℕ) where (_⌣_ {G'' = G} {n = 0} {1} ∣ (λ _ → g) ∣₂ ∣ S¹Fun embase (emloop h) ∣₂) ≡ RingStr._·_ (snd G) g h - help h = Iso.leftInv (Iso-EM-ΩEM+1 0) (RingStr._·_ (snd G) g h) + help h = Iso.ret (Iso-EM-ΩEM+1 0) (RingStr._·_ (snd G) g h) Hⁿ[Sⁿ,G]≅G-pres⌣ (suc n) G g = ST.elim (λ _ → isOfHLevelPath 2 (RingStr.is-set (snd G)) _ _) (Sⁿ-connElim n (isConnectedSubtr 2 (suc n) diff --git a/Cubical/Data/Bool/Properties.agda b/Cubical/Data/Bool/Properties.agda index f31da973f3..1454fbb75e 100644 --- a/Cubical/Data/Bool/Properties.agda +++ b/Cubical/Data/Bool/Properties.agda @@ -41,8 +41,8 @@ notnot false = refl notIso : Iso Bool Bool Iso.fun notIso = not Iso.inv notIso = not -Iso.rightInv notIso = notnot -Iso.leftInv notIso = notnot +Iso.sec notIso = notnot +Iso.ret notIso = notnot notIsEquiv : isEquiv not notIsEquiv = involIsEquiv {f = not} notnot @@ -234,8 +234,8 @@ module BoolReflection where reflectIso : Iso Bool (Bool ≡ Bool) reflectIso .fun = ⊕-Path reflectIso .inv P = transport P false - reflectIso .leftInv = ⊕-identityʳ - reflectIso .rightInv P = sym (⊕-complete P) + reflectIso .ret = ⊕-identityʳ + reflectIso .sec P = sym (⊕-complete P) reflectEquiv : Bool ≃ (Bool ≡ Bool) reflectEquiv = isoToEquiv reflectIso @@ -272,8 +272,8 @@ Iso.fun IsoBool→∙ f = fst f false fst (Iso.inv IsoBool→∙ a) false = a fst (Iso.inv (IsoBool→∙ {A = A}) a) true = pt A snd (Iso.inv IsoBool→∙ a) = refl -Iso.rightInv IsoBool→∙ a = refl -Iso.leftInv IsoBool→∙ (f , p) = +Iso.sec IsoBool→∙ a = refl +Iso.ret IsoBool→∙ (f , p) = ΣPathP ((funExt (λ { false → refl ; true → sym p})) , λ i j → p (~ i ∨ j)) @@ -399,10 +399,10 @@ Iso-⊤⊎⊤-Bool .fun (inl tt) = true Iso-⊤⊎⊤-Bool .fun (inr tt) = false Iso-⊤⊎⊤-Bool .inv true = inl tt Iso-⊤⊎⊤-Bool .inv false = inr tt -Iso-⊤⊎⊤-Bool .leftInv (inl tt) = refl -Iso-⊤⊎⊤-Bool .leftInv (inr tt) = refl -Iso-⊤⊎⊤-Bool .rightInv true = refl -Iso-⊤⊎⊤-Bool .rightInv false = refl +Iso-⊤⊎⊤-Bool .ret (inl tt) = refl +Iso-⊤⊎⊤-Bool .ret (inr tt) = refl +Iso-⊤⊎⊤-Bool .sec true = refl +Iso-⊤⊎⊤-Bool .sec false = refl separatedBool : Separated Bool separatedBool = Discrete→Separated _≟_ @@ -415,9 +415,9 @@ Bool→Bool→∙Bool true = const∙ _ _ Iso-Bool→∙Bool-Bool : Iso ((Bool , true) →∙ (Bool , true)) Bool Iso.fun Iso-Bool→∙Bool-Bool f = fst f false Iso.inv Iso-Bool→∙Bool-Bool = Bool→Bool→∙Bool -Iso.rightInv Iso-Bool→∙Bool-Bool false = refl -Iso.rightInv Iso-Bool→∙Bool-Bool true = refl -Iso.leftInv Iso-Bool→∙Bool-Bool f = Σ≡Prop (λ _ → isSetBool _ _) (help _ refl) +Iso.sec Iso-Bool→∙Bool-Bool false = refl +Iso.sec Iso-Bool→∙Bool-Bool true = refl +Iso.ret Iso-Bool→∙Bool-Bool f = Σ≡Prop (λ _ → isSetBool _ _) (help _ refl) where help : (x : Bool) → fst f false ≡ x → Bool→Bool→∙Bool (fst f false) .fst ≡ f .fst @@ -436,8 +436,8 @@ Iso.leftInv Iso-Bool→∙Bool-Bool f = Σ≡Prop (λ _ → isSetBool _ _) (help Iso.fun (ΣBoolΣIso {true}) x = tt , x Iso.inv (ΣBoolΣIso {true}) x = snd x -Iso.leftInv (ΣBoolΣIso {true}) _ = refl -Iso.rightInv (ΣBoolΣIso {true}) _ = refl +Iso.ret (ΣBoolΣIso {true}) _ = refl +Iso.sec (ΣBoolΣIso {true}) _ = refl ΣBool≃Σ : {b : Bool} {c : (Bool→Type b) → Bool} → (Bool→Type (ΣBool b c)) ≃ (Σ[ z ∈ Bool→Type b ] Bool→Type (c z)) diff --git a/Cubical/Data/Cardinal/Properties.agda b/Cubical/Data/Cardinal/Properties.agda index 0284c8350c..46c8c38f47 100644 --- a/Cubical/Data/Cardinal/Properties.agda +++ b/Cubical/Data/Cardinal/Properties.agda @@ -100,8 +100,8 @@ module _ where where iso⊥ : ∀ A → Iso (⊥* → A) Unit* Iso.fun (iso⊥ A) _ = tt* Iso.inv (iso⊥ A) _ () - Iso.rightInv (iso⊥ A) _ = refl - Iso.leftInv (iso⊥ A) _ i () + Iso.sec (iso⊥ A) _ = refl + Iso.ret (iso⊥ A) _ i () ^IdR𝟙 : (A : Card {ℓ}) → A ^ 𝟙 {ℓ} ≡ A ^IdR𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) @@ -110,8 +110,8 @@ module _ where where iso⊤ : ∀ A → Iso (Unit* → A) A Iso.fun (iso⊤ _) f = f tt* Iso.inv (iso⊤ _) a _ = a - Iso.rightInv (iso⊤ _) _ = refl - Iso.leftInv (iso⊤ _) _ = refl + Iso.sec (iso⊤ _) _ = refl + Iso.ret (iso⊤ _) _ = refl ^AnnihilL𝟙 : (A : Card {ℓ}) → 𝟙 {ℓ} ^ A ≡ 𝟙 {ℓ} ^AnnihilL𝟙 = ∥₂.elim (λ _ → isProp→isSet (isSetCard _ _)) @@ -120,8 +120,8 @@ module _ where where iso⊤ : ∀ A → Iso (A → Unit*) Unit* Iso.fun (iso⊤ _) _ = tt* Iso.inv (iso⊤ _) _ _ = tt* - Iso.rightInv (iso⊤ _) _ = refl - Iso.leftInv (iso⊤ _) _ = refl + Iso.sec (iso⊤ _) _ = refl + Iso.ret (iso⊤ _) _ = refl ^LDist+ : (A : Card {ℓa}) (B : Card {ℓb}) (C : Card {ℓc}) → A ^ (B + C) ≡ (A ^ B) · (A ^ C) diff --git a/Cubical/Data/Containers/Algebras.agda b/Cubical/Data/Containers/Algebras.agda index 86e0560237..62d81b920c 100644 --- a/Cubical/Data/Containers/Algebras.agda +++ b/Cubical/Data/Containers/Algebras.agda @@ -36,8 +36,8 @@ module Algs (S : Type ℓ) isom : Iso (Σ[ s ∈ S ] (Q s → W S Q)) (W S Q) fun isom = uncurry sup-W inv isom (sup-W s f) = s , f - rightInv isom (sup-W s f) = refl - leftInv isom (s , f) = refl + sec isom (sup-W s f) = refl + ret isom (s , f) = refl data Pos {Ind : Type ℓ'''} (P : Ind → S → Type ℓ'') (FP : ContFuncIso {ℓ}) (i : Ind) : carrier FP → Type (ℓ-max (ℓ-suc ℓ) (ℓ-max ℓ'' ℓ')) where diff --git a/Cubical/Data/Containers/ContainerExtensionProofs.agda b/Cubical/Data/Containers/ContainerExtensionProofs.agda index cb6a9fbf63..f60befc2e0 100644 --- a/Cubical/Data/Containers/ContainerExtensionProofs.agda +++ b/Cubical/Data/Containers/ContainerExtensionProofs.agda @@ -61,11 +61,11 @@ module _ {C : Category ℓ ℓ'} where (funExt₂ λ X (s , h) → sym (funExt⁻ (nat h) (s , C .id)) ∙ cong (λ Z → mors X (s , Z)) (C .⋆IdL h)) - ret : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y - ret (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i + ret' : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y + ret' (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i unique : (y : fiber (⟦_⟧-mor) (natTrans mors nat)) → (fib (natTrans mors nat) , fib-pf) ≡ y - unique (m , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _) (cong fib (sym m-eq) ∙ ret m) + unique (m , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _) (cong fib (sym m-eq) ∙ ret' m) -- Proof 2 that the functor ⟦_⟧ is full and faithful -- Uses the Yoneda lemma diff --git a/Cubical/Data/Empty/Properties.agda b/Cubical/Data/Empty/Properties.agda index 2ff52f19fe..f05aa263c7 100644 --- a/Cubical/Data/Empty/Properties.agda +++ b/Cubical/Data/Empty/Properties.agda @@ -32,5 +32,5 @@ uninhabEquiv ¬a ¬b = isoToEquiv isom isom : Iso _ _ isom .fun a = rec (¬a a) isom .inv b = rec (¬b b) - isom .rightInv b = rec (¬b b) - isom .leftInv a = rec (¬a a) + isom .sec b = rec (¬b b) + isom .ret a = rec (¬a a) diff --git a/Cubical/Data/Equality/Conversion.agda b/Cubical/Data/Equality/Conversion.agda index bd47adc779..52c48e6682 100644 --- a/Cubical/Data/Equality/Conversion.agda +++ b/Cubical/Data/Equality/Conversion.agda @@ -215,8 +215,8 @@ record Iso {ℓ ℓ'} (A : Type ℓ) (B : Type ℓ') : Type (ℓ-max ℓ ℓ') w field fun : A → B inv : B → A - rightInv : (b : B) → fun (inv b) ≡ b - leftInv : (a : A) → inv (fun a) ≡ a + sec : (b : B) → fun (inv b) ≡ b + ret : (a : A) → inv (fun a) ≡ a isoToIsoPath : Iso A B → IsoPath A B isoToIsoPath (iso f g η ε) = isoPath f g (λ b → eqToPath (η b)) (λ a → eqToPath (ε a)) diff --git a/Cubical/Data/Fin/Inductive/Properties.agda b/Cubical/Data/Fin/Inductive/Properties.agda index badbaf1ba1..f1d70a4343 100644 --- a/Cubical/Data/Fin/Inductive/Properties.agda +++ b/Cubical/Data/Fin/Inductive/Properties.agda @@ -134,9 +134,9 @@ sumFinGenId _+_ 0A f g p i = sumFinGen _+_ 0A (p i) Iso-Fin-InductiveFin : (m : ℕ) → Iso (FinOld.Fin m) (Fin m) Iso.fun (Iso-Fin-InductiveFin m) (x , p) = x , <→<ᵗ p Iso.inv (Iso-Fin-InductiveFin m) (x , p) = x , <ᵗ→< p -Iso.rightInv (Iso-Fin-InductiveFin m) (x , p) = +Iso.sec (Iso-Fin-InductiveFin m) (x , p) = Σ≡Prop (λ w → isProp<ᵗ {n = w} {m}) refl -Iso.leftInv (Iso-Fin-InductiveFin m) _ = Σ≡Prop (λ _ → OrderOld.isProp≤) refl +Iso.ret (Iso-Fin-InductiveFin m) _ = Σ≡Prop (λ _ → OrderOld.isProp≤) refl isSetFin : {n : ℕ} → isSet (Fin n) isSetFin {n = n} = @@ -165,20 +165,20 @@ inhabitedFibres?Fin {A = A} da (suc n) f y with da (f fzero) y Iso-Fin1⊎Fin-FinSuc : {n : ℕ} → Iso (Fin 1 ⊎ Fin n) (Fin (suc n)) Iso.fun (Iso-Fin1⊎Fin-FinSuc {n = n}) = ⊎.rec (λ _ → flast) injectSuc Iso.inv (Iso-Fin1⊎Fin-FinSuc {n = n}) = elimFin (inl flast) inr -Iso.rightInv (Iso-Fin1⊎Fin-FinSuc {n = n}) = +Iso.sec (Iso-Fin1⊎Fin-FinSuc {n = n}) = elimFin (cong (⊎.rec (λ _ → flast) injectSuc) (elimFinβ (inl flast) inr .fst)) λ x → cong (⊎.rec (λ _ → flast) injectSuc) (elimFinβ (inl flast) inr .snd x) -Iso.leftInv (Iso-Fin1⊎Fin-FinSuc {n = n}) (inl (zero , p)) = +Iso.ret (Iso-Fin1⊎Fin-FinSuc {n = n}) (inl (zero , p)) = elimFinβ (inl flast) inr .fst -Iso.leftInv (Iso-Fin1⊎Fin-FinSuc {n = n}) (inr x) = elimFinβ (inl flast) inr .snd x +Iso.ret (Iso-Fin1⊎Fin-FinSuc {n = n}) (inr x) = elimFinβ (inl flast) inr .snd x Iso-Fin⊎Fin-Fin+ : {n m : ℕ} → Iso (Fin n ⊎ Fin m) (Fin (n + m)) Iso.fun (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) (inr x) = x Iso.inv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) x = inr x -Iso.rightInv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) x = refl -Iso.leftInv (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) (inr x) = refl +Iso.sec (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) x = refl +Iso.ret (Iso-Fin⊎Fin-Fin+ {n = zero} {m = m}) (inr x) = refl Iso-Fin⊎Fin-Fin+ {n = suc n} {m = m} = compIso (⊎Iso (invIso Iso-Fin1⊎Fin-FinSuc) idIso) (compIso ⊎-assoc-Iso @@ -188,19 +188,19 @@ Iso-Fin⊎Fin-Fin+ {n = suc n} {m = m} = Iso-Unit-Fin1 : Iso Unit (Fin 1) Iso.fun Iso-Unit-Fin1 tt = fzero Iso.inv Iso-Unit-Fin1 (x , p) = tt -Iso.rightInv Iso-Unit-Fin1 (zero , p) = Σ≡Prop (λ _ → isProp<ᵗ) refl -Iso.leftInv Iso-Unit-Fin1 x = refl +Iso.sec Iso-Unit-Fin1 (zero , p) = Σ≡Prop (λ _ → isProp<ᵗ) refl +Iso.ret Iso-Unit-Fin1 x = refl Iso-Bool-Fin2 : Iso Bool (Fin 2) Iso.fun Iso-Bool-Fin2 false = flast Iso.fun Iso-Bool-Fin2 true = fzero Iso.inv Iso-Bool-Fin2 (zero , p) = true Iso.inv Iso-Bool-Fin2 (suc x , p) = false -Iso.rightInv Iso-Bool-Fin2 (zero , p) = refl -Iso.rightInv Iso-Bool-Fin2 (suc zero , p) = +Iso.sec Iso-Bool-Fin2 (zero , p) = refl +Iso.sec Iso-Bool-Fin2 (suc zero , p) = Σ≡Prop (λ _ → isProp<ᵗ) refl -Iso.leftInv Iso-Bool-Fin2 false = refl -Iso.leftInv Iso-Bool-Fin2 true = refl +Iso.ret Iso-Bool-Fin2 false = refl +Iso.ret Iso-Bool-Fin2 true = refl Iso-Fin×Fin-Fin· : {n m : ℕ} → Iso (Fin n × Fin m) (Fin (n · m)) Iso-Fin×Fin-Fin· {n = zero} {m = m} = @@ -224,10 +224,10 @@ fst (Iso.fun (Iso-FinSuc→-Fin→× n) f) x = f (fsuc x) snd (Iso.fun (Iso-FinSuc→-Fin→× n) f) = f fzero Iso.inv (Iso-FinSuc→-Fin→× n) (f , s) (zero , w) = s Iso.inv (Iso-FinSuc→-Fin→× (suc n)) (f , s) (suc t , w) = f (t , w) -fst (Iso.rightInv (Iso-FinSuc→-Fin→× (suc n)) (f , s) i) (w , t) = f (w , t) -snd (Iso.rightInv (Iso-FinSuc→-Fin→× n) (f , s) i) = s -Iso.leftInv (Iso-FinSuc→-Fin→× n) f i (zero , tt) = f fzero -Iso.leftInv (Iso-FinSuc→-Fin→× (suc n)) f i (suc s , t) = f (suc s , t) +fst (Iso.sec (Iso-FinSuc→-Fin→× (suc n)) (f , s) i) (w , t) = f (w , t) +snd (Iso.sec (Iso-FinSuc→-Fin→× n) (f , s) i) = s +Iso.ret (Iso-FinSuc→-Fin→× n) f i (zero , tt) = f fzero +Iso.ret (Iso-FinSuc→-Fin→× (suc n)) f i (suc s , t) = f (suc s , t) Iso-Fin×Bool-Fin : {n : ℕ} → Iso (Fin n × Bool) (Fin (2 · n)) Iso-Fin×Bool-Fin = @@ -245,9 +245,9 @@ module _ {m : ℕ} where Iso-Fin-Unit⊎Fin : Iso (Fin (suc m)) (Unit ⊎ Fin m) Iso.fun Iso-Fin-Unit⊎Fin = Fin→Unit⊎Fin Iso.inv Iso-Fin-Unit⊎Fin = Unit⊎Fin→Fin - Iso.rightInv Iso-Fin-Unit⊎Fin (inl x) = elimFinβ (inl tt) inr .fst - Iso.rightInv Iso-Fin-Unit⊎Fin (inr x) = elimFinβ (inl tt) inr .snd x - Iso.leftInv Iso-Fin-Unit⊎Fin = + Iso.sec Iso-Fin-Unit⊎Fin (inl x) = elimFinβ (inl tt) inr .fst + Iso.sec Iso-Fin-Unit⊎Fin (inr x) = elimFinβ (inl tt) inr .snd x + Iso.ret Iso-Fin-Unit⊎Fin = elimFin (cong Unit⊎Fin→Fin (elimFinβ (inl tt) inr .fst)) λ x → (cong Unit⊎Fin→Fin (elimFinβ (inl tt) inr .snd x)) @@ -308,8 +308,8 @@ module _ {n : ℕ} where swapFinIso : (x y : Fin n) → Iso (Fin n) (Fin n) Iso.fun (swapFinIso x y) = swapFin x y Iso.inv (swapFinIso x y) = swapFin x y - Iso.rightInv (swapFinIso x y) = swapFin² x y - Iso.leftInv (swapFinIso x y) = swapFin² x y + Iso.sec (swapFinIso x y) = swapFin² x y + Iso.ret (swapFinIso x y) = swapFin² x y module _ {ℓ : Level} {n : ℕ} {A : Fin n → Type ℓ} (x₀ : Fin n) (pt : A x₀) (l : (x : Fin n) → ¬ x ≡ x₀ → A x) where diff --git a/Cubical/Data/Fin/LehmerCode.agda b/Cubical/Data/Fin/LehmerCode.agda index 86622ae7b5..6647a95753 100644 --- a/Cubical/Data/Fin/LehmerCode.agda +++ b/Cubical/Data/Fin/LehmerCode.agda @@ -59,13 +59,13 @@ projectionEquiv {n = n} {i = i} = isoToEquiv goal where goal .Iso.fun (inl _) = i goal .Iso.fun (inr m) = fst m goal .Iso.inv m = case discreteFin i m of λ { (yes _) → inl tt ; (no n) → inr (m , n) } - goal .Iso.rightInv m with discreteFin i m + goal .Iso.sec m with discreteFin i m ... | (yes p) = p ... | (no _) = toℕ-injective refl - goal .Iso.leftInv (inl tt) with discreteFin i i + goal .Iso.ret (inl tt) with discreteFin i i ... | (yes _) = refl ... | (no ¬ii) = ⊥.rec (¬ii refl) - goal .Iso.leftInv (inr m) with discreteFin i (fst m) + goal .Iso.ret (inr m) with discreteFin i (fst m) ... | (yes p) = ⊥.rec (snd m p) ... | (no _) = cong inr (toℕExc-injective refl) @@ -170,9 +170,9 @@ lehmerEquiv {suc n} = (Σ[ k ∈ Fin (suc n) ] (FinExcept (fzero {k = n}) ≃ FinExcept k)) Iso.fun i f = equivFun f fzero , equivIn f Iso.inv i (k , f) = equivOut f - Iso.rightInv i (k , f) = ΣPathP (refl , equivEq (funExt λ x → + Iso.sec i (k , f) = ΣPathP (refl , equivEq (funExt λ x → toℕExc-injective (cong toℕ (equivOutChar {f = f} x)))) - Iso.leftInv i f = equivEq (funExt goal) where + Iso.ret i f = equivEq (funExt goal) where goal : ∀ x → equivFun (equivOut (equivIn f)) x ≡ equivFun f x goal x = case fsplit x return (λ _ → equivFun (equivOut (equivIn f)) x ≡ equivFun f x) of λ { (inl xz) → subst (λ x → equivFun (equivOut (equivIn f)) x ≡ equivFun f x) xz refl diff --git a/Cubical/Data/Fin/Properties.agda b/Cubical/Data/Fin/Properties.agda index b4366f20e7..2c44668db7 100644 --- a/Cubical/Data/Fin/Properties.agda +++ b/Cubical/Data/Fin/Properties.agda @@ -570,7 +570,7 @@ Iso.inv (Fin+≅Fin⊎Fin m n) = g g : Fin m ⊎ Fin n → Fin (m + n) g (inl (k , k