From e60d022ec5dfe66c17cc9226576e6c4f3b647306 Mon Sep 17 00:00:00 2001 From: mortberg Date: Fri, 3 Nov 2023 13:48:56 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20agda/cub?= =?UTF-8?q?ical@f8d6fcf3bc24ce3915b3960ad3b716fd082e8b9d=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical.Algebra.Algebra.Properties.html | 6 +- Cubical.Algebra.CommAlgebra.Properties.html | 6 +- Cubical.Algebra.CommRing.Properties.html | 6 +- ...l.Algebra.DirectSum.Equiv-DSHIT-DSFun.html | 2 +- Cubical.Algebra.GradedRing.DirectSumFun.html | 4 +- Cubical.Algebra.Group.GroupPath.html | 6 +- Cubical.Algebra.Ring.Properties.html | 6 +- ...Categories.Constructions.Free.Functor.html | 6 +- ...l.Categories.Constructions.Slice.Base.html | 6 +- Cubical.Categories.Displayed.Reasoning.html | 2 +- Cubical.Categories.Instances.Discrete.html | 4 +- Cubical.Codata.Conat.Bounded.html | 4 +- Cubical.Codata.Conat.Properties.html | 2 +- Cubical.Codata.M.AsLimit.M.Base.html | 8 +- Cubical.Codata.M.AsLimit.helper.html | 2 +- Cubical.Codata.M.Bisimilarity.html | 2 +- Cubical.Cohomology.EilenbergMacLane.Base.html | 4 +- ...ohomology.EilenbergMacLane.CupProduct.html | 6 +- ...cal.Cohomology.EilenbergMacLane.Gysin.html | 16 +- ...mology.EilenbergMacLane.RingStructure.html | 2 +- Cubical.Data.Bool.Properties.html | 8 +- Cubical.Data.Equality.Univalence.html | 2 +- Cubical.Data.Fin.Properties.html | 10 +- Cubical.Data.Fin.Recursive.Properties.html | 4 +- Cubical.Data.FinSet.Binary.Large.html | 2 +- ...l.Data.FinSet.Binary.Small.Properties.html | 12 +- Cubical.Data.FinSet.Cardinality.html | 10 +- Cubical.Data.FinSet.Constructors.html | 4 +- Cubical.Data.FinSet.Properties.html | 2 +- Cubical.Data.FinSet.Quotients.html | 2 +- Cubical.Data.Int.MoreInts.QuoInt.Base.html | 6 +- Cubical.Data.Int.Properties.html | 4 +- Cubical.Data.List.Dependent.html | 2 +- Cubical.Data.Nat.Algebra.html | 4 +- Cubical.Data.Nat.Lower.html | 2 +- Cubical.Data.Nat.Order.Recursive.html | 4 +- Cubical.Data.Nat.Properties.html | 2 +- Cubical.Data.Sigma.Properties.html | 4 +- Cubical.Data.SumFin.Properties.html | 2 +- Cubical.Displayed.Base.html | 2 +- Cubical.Displayed.Generic.html | 2 +- Cubical.Displayed.Morphism.html | 2 +- Cubical.Displayed.Properties.html | 4 +- Cubical.Displayed.Subst.html | 2 +- Cubical.Displayed.Universe.html | 4 +- Cubical.Experiments.EscardoSIP.html | 24 +- Cubical.Experiments.FunExtFromUA.html | 2 +- ...periments.ZCohomologyOld.KcompPrelims.html | 2 +- Cubical.Foundations.CartesianKanOps.html | 2 +- Cubical.Foundations.Equiv.Base.html | 34 ++ Cubical.Foundations.Equiv.Dependent.html | 2 +- Cubical.Foundations.Equiv.Properties.html | 8 +- Cubical.Foundations.Everything.html | 51 +-- Cubical.Foundations.HLevels.html | 12 +- Cubical.Foundations.Path.html | 12 +- Cubical.Foundations.Pointed.Homotopy.html | 2 +- Cubical.Foundations.SIP.html | 18 +- Cubical.Foundations.Transport.html | 399 +++++++++--------- Cubical.Foundations.Univalence.Dependent.html | 2 +- Cubical.Foundations.Univalence.Universe.html | 116 ++--- Cubical.Foundations.Univalence.html | 321 +++++++------- Cubical.Functions.Bundle.html | 2 +- Cubical.Functions.Embedding.html | 14 +- Cubical.Functions.Fibration.html | 2 +- Cubical.Functions.Involution.html | 2 +- ...al.HITs.Bouquet.FundamentalGroupProof.html | 4 +- ...cal.HITs.FreeGroupoid.GroupoidActions.html | 4 +- Cubical.HITs.James.Inductive.Reduced.html | 2 +- Cubical.HITs.Nullification.Properties.html | 2 +- Cubical.HITs.Pushout.Properties.html | 12 +- Cubical.HITs.RPn.Base.html | 2 +- Cubical.HITs.SmashProduct.Base.html | 2 +- Cubical.Homotopy.Connected.html | 10 +- ....Homotopy.EilenbergMacLane.CupProduct.html | 6 +- ...opy.EilenbergMacLane.GradedCommTensor.html | 12 +- Cubical.Homotopy.EilenbergMacLane.Order2.html | 2 +- ....Homotopy.EilenbergMacLane.Properties.html | 12 +- Cubical.Homotopy.Group.Base.html | 4 +- Cubical.Homotopy.Hopf.html | 4 +- Cubical.Homotopy.HopfInvariant.HopfMap.html | 2 +- Cubical.Homotopy.Loopspace.html | 2 +- Cubical.Homotopy.WhiteheadsLemma.html | 12 +- Cubical.Modalities.Lex.html | 2 +- Cubical.Papers.Pi4S3.html | 4 +- ...cal.Papers.RepresentationIndependence.html | 2 +- Cubical.Papers.ZCohomology.html | 2 +- Cubical.Relation.Binary.Extensionality.html | 2 +- Cubical.Structures.Function.html | 4 +- Cubical.Structures.Transfer.html | 2 +- Cubical.ZCohomology.CohomologyRings.CP2.html | 6 +- ....CohomologyRings.CupProductProperties.html | 4 +- Cubical.ZCohomology.CohomologyRings.RP2.html | 4 +- ...ZCohomology.CohomologyRings.S2wedgeS4.html | 6 +- Cubical.ZCohomology.CohomologyRings.Sn.html | 8 +- Cubical.ZCohomology.Groups.KleinBottle.html | 6 +- Cubical.ZCohomology.Groups.RP2.html | 2 +- Cubical.ZCohomology.Gysin.html | 6 +- Cubical.ZCohomology.Properties.html | 8 +- ...homology.RingStructure.CohomologyRing.html | 2 +- ...ogy.RingStructure.GradedCommutativity.html | 10 +- 100 files changed, 727 insertions(+), 676 deletions(-) diff --git a/Cubical.Algebra.Algebra.Properties.html b/Cubical.Algebra.Algebra.Properties.html index cf880b3f0d..78a7c1636c 100644 --- a/Cubical.Algebra.Algebra.Properties.html +++ b/Cubical.Algebra.Algebra.Properties.html @@ -216,9 +216,9 @@ caracAlgebra≡ : (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q caracAlgebra≡ {A = A} {B = B} p q P = - sym (transportTransport⁻ (ua (Algebra≡ A B)) p) + sym (transportTransport⁻ (ua (Algebra≡ A B)) p) ∙∙ cong (transport (ua (Algebra≡ A B))) helper - ∙∙ transportTransport⁻ (ua (Algebra≡ A B)) q + ∙∙ transportTransport⁻ (ua (Algebra≡ A B)) q where helper : transport (sym (ua (Algebra≡ A B))) p ≡ transport (sym (ua (Algebra≡ A B))) q helper = Σ≡Prop @@ -236,7 +236,7 @@ → uaAlgebra (compAlgebraEquiv f g) ≡ uaAlgebra f ∙ uaAlgebra g uaCompAlgebraEquiv f g = caracAlgebra≡ _ _ ( cong ⟨_⟩ (uaAlgebra (compAlgebraEquiv f g)) - ≡⟨ uaCompEquiv _ _ ⟩ + ≡⟨ uaCompEquiv _ _ ⟩ cong ⟨_⟩ (uaAlgebra f) ∙ cong ⟨_⟩ (uaAlgebra g) ≡⟨ sym (cong-∙ ⟨_⟩ (uaAlgebra f) (uaAlgebra g)) ⟩ cong ⟨_⟩ (uaAlgebra f ∙ uaAlgebra g) ∎) diff --git a/Cubical.Algebra.CommAlgebra.Properties.html b/Cubical.Algebra.CommAlgebra.Properties.html index e5369fecaf..e8e642dff5 100644 --- a/Cubical.Algebra.CommAlgebra.Properties.html +++ b/Cubical.Algebra.CommAlgebra.Properties.html @@ -261,9 +261,9 @@ caracCommAlgebra≡ : {A B : CommAlgebra R ℓ'} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q caracCommAlgebra≡ {A = A} {B = B} p q P = - sym (transportTransport⁻ (ua (CommAlgebra≡ A B)) p) + sym (transportTransport⁻ (ua (CommAlgebra≡ A B)) p) ∙∙ cong (transport (ua (CommAlgebra≡ A B))) helper - ∙∙ transportTransport⁻ (ua (CommAlgebra≡ A B)) q + ∙∙ transportTransport⁻ (ua (CommAlgebra≡ A B)) q where helper : transport (sym (ua (CommAlgebra≡ A B))) p ≡ transport (sym (ua (CommAlgebra≡ A B))) q helper = Σ≡Prop @@ -281,7 +281,7 @@ → uaCommAlgebra (compCommAlgebraEquiv f g) ≡ uaCommAlgebra f ∙ uaCommAlgebra g uaCompCommAlgebraEquiv f g = caracCommAlgebra≡ _ _ ( cong ⟨_⟩ (uaCommAlgebra (compCommAlgebraEquiv f g)) - ≡⟨ uaCompEquiv _ _ ⟩ + ≡⟨ uaCompEquiv _ _ ⟩ cong ⟨_⟩ (uaCommAlgebra f) ∙ cong ⟨_⟩ (uaCommAlgebra g) ≡⟨ sym (cong-∙ ⟨_⟩ (uaCommAlgebra f) (uaCommAlgebra g)) ⟩ cong ⟨_⟩ (uaCommAlgebra f ∙ uaCommAlgebra g) ∎) diff --git a/Cubical.Algebra.CommRing.Properties.html b/Cubical.Algebra.CommRing.Properties.html index a35c797c86..1462732d48 100644 --- a/Cubical.Algebra.CommRing.Properties.html +++ b/Cubical.Algebra.CommRing.Properties.html @@ -324,9 +324,9 @@ caracCommRing≡ : {A B : CommRing ℓ} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q caracCommRing≡ {A = A} {B = B} p q P = - sym (transportTransport⁻ (ua (CommRing≡ A B)) p) + sym (transportTransport⁻ (ua (CommRing≡ A B)) p) ∙∙ cong (transport (ua (CommRing≡ A B))) helper - ∙∙ transportTransport⁻ (ua (CommRing≡ A B)) q + ∙∙ transportTransport⁻ (ua (CommRing≡ A B)) q where helper : transport (sym (ua (CommRing≡ A B))) p ≡ transport (sym (ua (CommRing≡ A B))) q helper = Σ≡Prop @@ -343,7 +343,7 @@ → uaCommRing (compCommRingEquiv f g) ≡ uaCommRing f ∙ uaCommRing g uaCompCommRingEquiv f g = caracCommRing≡ _ _ ( cong ⟨_⟩ (uaCommRing (compCommRingEquiv f g)) - ≡⟨ uaCompEquiv _ _ ⟩ + ≡⟨ uaCompEquiv _ _ ⟩ cong ⟨_⟩ (uaCommRing f) ∙ cong ⟨_⟩ (uaCommRing g) ≡⟨ sym (cong-∙ ⟨_⟩ (uaCommRing f) (uaCommRing g)) ⟩ cong ⟨_⟩ (uaCommRing f ∙ uaCommRing g) ∎) diff --git a/Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun.html b/Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun.html index 5e51fefebe..f978f26ac0 100644 --- a/Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun.html +++ b/Cubical.Algebra.DirectSum.Equiv-DSHIT-DSFun.html @@ -388,7 +388,7 @@ lemmakk zero a = cong (base 0) (transportRefl a) lemmakk (suc k) a with (discreteℕ (suc k) (suc k)) | (discreteℕ k k) ... | yes p | yes q = cong₂ _add_ - (sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base (cong suc q) a)) + (sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base (cong suc q) a)) (lemmaSkk (suc k) a k ≤-refl) ∙ +⊕HIT-IdR _ ... | yes p | no ¬q = ⊥.rec (¬q refl) diff --git a/Cubical.Algebra.GradedRing.DirectSumFun.html b/Cubical.Algebra.GradedRing.DirectSumFun.html index 7bd87305b4..f6f7a72fef 100644 --- a/Cubical.Algebra.GradedRing.DirectSumFun.html +++ b/Cubical.Algebra.GradedRing.DirectSumFun.html @@ -297,7 +297,7 @@ sumFun i n r (fun-trad k a) (fun-trad l b) ≡ subst G pp (a ⋆ b) sumFun≤ k a l b zero n r pp rr with discreteℕ k 0 | discreteℕ l n ... | yes p | yes q = cong (subst G (sameFiber r)) (subst⋆ p q (pp ∙ sym (+nIdL _)) a b) - ∙ sym (substComposite G _ _ _) + ∙ sym (substComposite G _ _ _) ∙ cong (λ X → subst G X (a ⋆ b)) (isSetℕ _ _ _ _) ... | yes p | no ¬q = ⊥.rec (¬q (sym (+nIdL l) ∙ cong (λ X → X +n l) (sym p) ∙ pp)) ... | no ¬p | yes q = ⊥.rec (¬p (≤0→≡0 rr)) @@ -306,7 +306,7 @@ ... | yes p | yes q = cong₂ (Gstr n ._+_) (cong (subst G (sameFiber r)) (subst⋆ p q (pp ∙ sym (sameFiber r)) a b) - ∙ sym (substComposite G _ _ _)) + ∙ sym (substComposite G _ _ _)) (sumFun< k a l b i n (≤-trans ≤-sucℕ r) (0 , (sym p))) ∙ +IdR (Gstr n) _ ∙ cong (λ X → subst G X (a ⋆ b)) (isSetℕ _ _ _ _) diff --git a/Cubical.Algebra.Group.GroupPath.html b/Cubical.Algebra.Group.GroupPath.html index 44cbc150b8..7bf5ffb696 100644 --- a/Cubical.Algebra.Group.GroupPath.html +++ b/Cubical.Algebra.Group.GroupPath.html @@ -155,9 +155,9 @@ caracGroup≡ : {G H : Group ℓ} (p q : G ≡ H) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q caracGroup≡ {G = G} {H = H} p q P = - sym (transportTransport⁻ (ua (Group≡ G H)) p) + sym (transportTransport⁻ (ua (Group≡ G H)) p) ∙∙ cong (transport (ua (Group≡ G H))) helper - ∙∙ transportTransport⁻ (ua (Group≡ G H)) q + ∙∙ transportTransport⁻ (ua (Group≡ G H)) q where helper : transport (sym (ua (Group≡ G H))) p ≡ transport (sym (ua (Group≡ G H))) q helper = Σ≡Prop @@ -175,7 +175,7 @@ → uaGroup (compGroupEquiv f g) ≡ uaGroup f ∙ uaGroup g uaCompGroupEquiv f g = caracGroup≡ _ _ ( cong ⟨_⟩ (uaGroup (compGroupEquiv f g)) - ≡⟨ uaCompEquiv _ _ ⟩ + ≡⟨ uaCompEquiv _ _ ⟩ cong ⟨_⟩ (uaGroup f) ∙ cong ⟨_⟩ (uaGroup g) ≡⟨ sym (cong-∙ ⟨_⟩ (uaGroup f) (uaGroup g)) ⟩ cong ⟨_⟩ (uaGroup f ∙ uaGroup g) ∎) diff --git a/Cubical.Algebra.Ring.Properties.html b/Cubical.Algebra.Ring.Properties.html index 8ea342c6ab..48f7ffa89e 100644 --- a/Cubical.Algebra.Ring.Properties.html +++ b/Cubical.Algebra.Ring.Properties.html @@ -291,9 +291,9 @@ caracRing≡ : {A B : Ring ℓ} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q caracRing≡ {A = A} {B = B} p q P = - sym (transportTransport⁻ (ua (Ring≡ A B)) p) + sym (transportTransport⁻ (ua (Ring≡ A B)) p) ∙∙ cong (transport (ua (Ring≡ A B))) helper - ∙∙ transportTransport⁻ (ua (Ring≡ A B)) q + ∙∙ transportTransport⁻ (ua (Ring≡ A B)) q where helper : transport (sym (ua (Ring≡ A B))) p ≡ transport (sym (ua (Ring≡ A B))) q helper = Σ≡Prop @@ -310,7 +310,7 @@ → uaRing (compRingEquiv f g) ≡ uaRing f ∙ uaRing g uaCompRingEquiv f g = caracRing≡ _ _ ( cong ⟨_⟩ (uaRing (compRingEquiv f g)) - ≡⟨ uaCompEquiv _ _ ⟩ + ≡⟨ uaCompEquiv _ _ ⟩ cong ⟨_⟩ (uaRing f) ∙ cong ⟨_⟩ (uaRing g) ≡⟨ sym (cong-∙ ⟨_⟩ (uaRing f) (uaRing g)) ⟩ cong ⟨_⟩ (uaRing f ∙ uaRing g) ∎) diff --git a/Cubical.Categories.Constructions.Free.Functor.html b/Cubical.Categories.Constructions.Free.Functor.html index 61b2d0efff..1b8e8a7c7f 100644 --- a/Cubical.Categories.Constructions.Free.Functor.html +++ b/Cubical.Categories.Constructions.Free.Functor.html @@ -249,16 +249,16 @@ (𝓕 ⟪ semG ⟪ e ⟫ ⟫)) pathified = toPathP⁻ (( fromPathP⁻ lem' - ∙ cong (transport⁻ (λ i → 𝓓 [ arb𝓕 (~ i) ⟅ v ⟆ + ∙ cong (transport⁻ (λ i → 𝓓 [ arb𝓕 (~ i) ⟅ v ⟆ , arb𝓕 (~ i) ⟅ w ⟆ ])) (fromPathP⁻ lem𝓒) - ∙ sym (transportComposite + ∙ sym (transportComposite ((λ i → 𝓓 [ 𝓕 ⟅ arb𝓒-agree (~ i) $g v ⟆ , 𝓕 ⟅ arb𝓒-agree (~ i) $g w ⟆ ])) (λ i → 𝓓 [ arb𝓕 i ⟅ v ⟆ , arb𝓕 i ⟅ w ⟆ ]) ((𝓕 ⟪ semG ⟪ e ⟫ ⟫))) ∙ ((λ i → transport (substOf-sems-agreeϕ i) (𝓕 ⟪ semG ⟪ e ⟫ ⟫))) - ∙ transportComposite + ∙ transportComposite (λ i → 𝓓 [ ıϕp i v , ıϕp i w ]) (λ i → 𝓓 [ arb𝓓-agree (~ i) $g ϕ v , arb𝓓-agree (~ i) $g ϕ w ]) diff --git a/Cubical.Categories.Constructions.Slice.Base.html b/Cubical.Categories.Constructions.Slice.Base.html index d862c533d4..8ed659f521 100644 --- a/Cubical.Categories.Constructions.Slice.Base.html +++ b/Cubical.Categories.Constructions.Slice.Base.html @@ -6,7 +6,7 @@ open import Cubical.Foundations.Equiv open import Cubical.Foundations.HLevels open import Cubical.Foundations.Univalence -open import Cubical.Foundations.Transport using (transpFill) +open import Cubical.Foundations.Transport using (transpFill) open import Cubical.Categories.Category renaming (isIso to isIsoC) open import Cubical.Categories.Morphism @@ -349,10 +349,10 @@ -- using the computation rule to ua p'ΣT≡p'Σ : p'ΣT ≡ p'Σ - p'ΣT≡p'Σ = uaβ SOPath≃PathΣ p' + p'ΣT≡p'Σ = uaβ SOPath≃PathΣ p' pΣT≡pΣ : pΣT ≡ pΣ - pΣT≡pΣ = uaβ SOPath≃PathΣ p + pΣT≡pΣ = uaβ SOPath≃PathΣ p p'Σ≡pΣ : p'Σ ≡ pΣ p'Σ≡pΣ = ΣPathP (p'Ob≡pOb , p'Mor≡pMor) diff --git a/Cubical.Categories.Displayed.Reasoning.html b/Cubical.Categories.Displayed.Reasoning.html index 1070afced5..d122c62e2a 100644 --- a/Cubical.Categories.Displayed.Reasoning.html +++ b/Cubical.Categories.Displayed.Reasoning.html @@ -91,7 +91,7 @@ {aᴰ : ob[ a ]} {bᴰ : ob[ b ]} {fᴰ : Hom[ f ][ aᴰ , bᴰ ]} → reind (p ∙ q) fᴰ ≡ reind q (reind p fᴰ) - reind-comp = substComposite Hom[_][ _ , _ ] _ _ _ + reind-comp = substComposite Hom[_][ _ , _ ] _ _ _ reind-contractˡ : {a b c : C.ob} {f : C [ a , b ]} {g h : C [ b , c ]} {p : g ≡ h} diff --git a/Cubical.Categories.Instances.Discrete.html b/Cubical.Categories.Instances.Discrete.html index 51650ed1b7..d595781e20 100644 --- a/Cubical.Categories.Instances.Discrete.html +++ b/Cubical.Categories.Instances.Discrete.html @@ -50,8 +50,8 @@ let id-fy = id C {f y} in let Fp = (subst Hom[fx,f—] (p) id-fx) in - subst Hom[fx,f—] (p ∙ q) id-fx ≡⟨ substComposite Hom[fx,f—] _ _ _ ⟩ + subst Hom[fx,f—] (p ∙ q) id-fx ≡⟨ substComposite Hom[fx,f—] _ _ _ ⟩ subst Hom[fx,f—] (q) (Fp) ≡⟨ cong (subst _ q) (sym (⋆IdR C _)) ⟩ - subst Hom[fx,f—] (q) (Fp ● id-fy) ≡⟨ substCommSlice _ _ (λ _ → Fp ●_) q _ ⟩ + subst Hom[fx,f—] (q) (Fp ● id-fy) ≡⟨ substCommSlice _ _ (λ _ → Fp ●_) q _ ⟩ Fp ● (subst Hom[fy,f—] (q) id-fy) ∎ \ No newline at end of file diff --git a/Cubical.Codata.Conat.Bounded.html b/Cubical.Codata.Conat.Bounded.html index d5517e193c..c1ec1f370b 100644 --- a/Cubical.Codata.Conat.Bounded.html +++ b/Cubical.Codata.Conat.Bounded.html @@ -133,7 +133,7 @@ ... | csuc o | czero = Empty.rec {A = csuc o ≡ czero} (transport (∀≺ 0) _) i ... | czero | csuc p - = Empty.rec {A = czero ≡ csuc p} (transport⁻ (∀≺ 0) _) i + = Empty.rec {A = czero ≡ csuc p} (transport⁻ (∀≺ 0) _) i Bounded→Fin : ∀ m → Bounded (embed m) → Fin.Fin m Bounded→Fin (suc m) (0 , 0≺m) = Fin.zero @@ -247,5 +247,5 @@ = rec {A = csuc l ≡ czero} (Iso.fun theIso (zero , _) .snd) i Bounded-inj : ∀ m n → Bounded m ≡ Bounded n → m ≡ n -Bounded-inj m n = Bounded-inj-iso m n ∘ pathToIso +Bounded-inj m n = Bounded-inj-iso m n ∘ pathToIso \ No newline at end of file diff --git a/Cubical.Codata.Conat.Properties.html b/Cubical.Codata.Conat.Properties.html index 0d9bce8513..5233a13a0d 100644 --- a/Cubical.Codata.Conat.Properties.html +++ b/Cubical.Codata.Conat.Properties.html @@ -286,5 +286,5 @@ lpo' α = disc (uncover (search α)) refl where disc : ∀ n → uncover (search α) ≡ n → _ disc Nat.zero p = inl λ n → subst ⟨_⟩ (search-0 α p n) - disc (Nat.suc n) p = inr (n , subst⁻ ⟨_⟩ (search-n' α n p) _) + disc (Nat.suc n) p = inr (n , subst⁻ ⟨_⟩ (search-n' α n p) _) \ No newline at end of file diff --git a/Cubical.Codata.M.AsLimit.M.Base.html b/Cubical.Codata.M.AsLimit.M.Base.html index 7bdb98392a..78fa471feb 100644 --- a/Cubical.Codata.M.AsLimit.M.Base.html +++ b/Cubical.Codata.M.AsLimit.M.Base.html @@ -127,11 +127,11 @@ ≡ transp (λ j → B (α-iso-step-5-Iso-helper0 a p n (i ∧ j)) → Wₙ S n) (~ i) (u n)) ⟩ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (subst (λ k → B k → Wₙ S n) (p n) (πₙ S ∘ u (suc n))) ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n) - ≡⟨ (λ i → sym (substComposite (λ k → B k → Wₙ S n) (p n) (α-iso-step-5-Iso-helper0 a p n) (πₙ S ∘ u (suc n))) i + ≡⟨ (λ i → sym (substComposite (λ k → B k → Wₙ S n) (p n) (α-iso-step-5-Iso-helper0 a p n) (πₙ S ∘ u (suc n))) i ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p (suc n)) (πₙ S ∘ u (suc n)) ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n) - ≡⟨ (λ i → substCommSlice (λ k → B k → Wₙ S (suc n)) (λ k → B k → Wₙ S n) + ≡⟨ (λ i → substCommSlice (λ k → B k → Wₙ S (suc n)) (λ k → B k → Wₙ S n) (λ a x x₁ → (πₙ S) (x x₁)) (α-iso-step-5-Iso-helper0 a p (suc n)) (u (suc n)) i ≡ subst (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 a p n) (u n)) ⟩ @@ -149,8 +149,8 @@ (Σ[ a ∈ A ] (Σ[ u ∈ ((n : ℕ) → B a → X (sequence S) n) ] ((n : ℕ) → π (sequence S) ∘ (u (suc n)) ≡ u n))) α-iso-step-5-Iso = Σ-cong-iso (lemma11-Iso {S = S} (λ _ → A) (λ _ x → x)) (λ a,p → - Σ-cong-iso (pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → cong (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 (a,p .fst) (a,p .snd) n)))) λ u → - pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → α-iso-step-5-Iso-helper1-Iso (a,p .fst) (a,p .snd) u n))) + Σ-cong-iso (pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → cong (λ k → B k → Wₙ S n) (α-iso-step-5-Iso-helper0 (a,p .fst) (a,p .snd) n)))) λ u → + pathToIso (cong (λ k → (n : ℕ) → k n) (funExt λ n → α-iso-step-5-Iso-helper1-Iso (a,p .fst) (a,p .snd) u n))) α-iso-step-1-4-Iso-lem-12 : Iso (Σ[ a ∈ (Σ[ a ∈ ((n : ℕ) → A)] ((n : ℕ) → a (suc n) ≡ a n)) ] diff --git a/Cubical.Codata.M.AsLimit.helper.html b/Cubical.Codata.M.AsLimit.helper.html index 1dce05dbc6..1b0f3c216f 100644 --- a/Cubical.Codata.M.AsLimit.helper.html +++ b/Cubical.Codata.M.AsLimit.helper.html @@ -40,7 +40,7 @@ → ∀ {f g : C -> A} → Iso (∀ x → (fun isom) (f x) ≡ (fun isom) (g x)) (∀ x → f x ≡ g x) iso→Pi-fun-Injection {A = A} {B} {C} isom {f = f} {g} = - pathToIso (cong (λ k → ∀ x → k x) (funExt (iso→fun-Injection isom {f = f} {g = g}))) + pathToIso (cong (λ k → ∀ x → k x) (funExt (iso→fun-Injection isom {f = f} {g = g}))) iso→fun-Injection-Iso : ∀ {ℓ} {A B C : Type ℓ} (isom : Iso A B) diff --git a/Cubical.Codata.M.Bisimilarity.html b/Cubical.Codata.M.Bisimilarity.html index 8b1bd8bf6b..4fb3f1726e 100644 --- a/Cubical.Codata.M.Bisimilarity.html +++ b/Cubical.Codata.M.Bisimilarity.html @@ -136,7 +136,7 @@ , u _ .snd .tails≈ y (transp (λ k → C .snd x (u _ .snd .head≈ (~ k ∧ l)) y) (~ l) (peq l)) pb \ j → lemma (C .snd x (u 1=1 .fst .head) y) (λ h → C .snd x (eqh h) y) pa pb peq l j) z) - (transpFill {A = F i0} i0 (\ i → inS (F i)) u0 l) + (transpFill {A = F i0} i0 (\ i → inS (F i)) u0 l) (u _ .snd .tails≈ y pa pb peq)) r i diff --git a/Cubical.Cohomology.EilenbergMacLane.Base.html b/Cubical.Cohomology.EilenbergMacLane.Base.html index 4a54cad138..6b5c781278 100644 --- a/Cubical.Cohomology.EilenbergMacLane.Base.html +++ b/Cubical.Cohomology.EilenbergMacLane.Base.html @@ -315,7 +315,7 @@ → (p : n ≡ m) → AbGroupEquiv (coHomGr n G A) (coHomGr m G A) fst (substℕ-coHom {A = A} {G = G} p) = - substEquiv' (λ i → coHom i G A) p + substEquiv' (λ i → coHom i G A) p snd (substℕ-coHom {A = A} {G = G} p) = makeIsGroupHom λ x y → @@ -329,7 +329,7 @@ → (p : n ≡ m) → AbGroupEquiv (coHomRedGr n G A) (coHomRedGr m G A) fst (substℕ-coHomRed {A = A} {G = G} p) = - substEquiv' (λ i → coHomRed i G A) p + substEquiv' (λ i → coHomRed i G A) p snd (substℕ-coHomRed {A = A} {G = G} p) = makeIsGroupHom λ x y → diff --git a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html index deec2edb1e..e1d2dfe7b0 100644 --- a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html +++ b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html @@ -193,13 +193,13 @@ ⌣-1ₕDep : (n : ℕ) (x : coHom n G' A) → PathP (λ i → coHom (+'-comm zero n (~ i)) G' A) (x ⌣ 1ₕ) x ⌣-1ₕDep n x = toPathP {A = λ i → coHom (+'-comm zero n (~ i)) G' A} - (flipTransport (⌣-1ₕ n x)) + (flipTransport (⌣-1ₕ n x)) assoc⌣Dep : (n m l : ℕ) (x : coHom n G' A) (y : coHom m G' A) (z : coHom l G' A) → PathP (λ i → coHom (+'-assoc n m l (~ i)) G' A) ((x ⌣ y) ⌣ z) (x ⌣ (y ⌣ z)) assoc⌣Dep n m l x y z = toPathP {A = λ i → coHom (+'-assoc n m l (~ i)) G' A} - (flipTransport (assoc⌣ n m l x y z)) + (flipTransport (assoc⌣ n m l x y z)) module _ {G'' : CommRing ℓ} {A : Type ℓ'} where private @@ -209,5 +209,5 @@ (x ⌣ y) (-ₕ^[ n · m ] (y ⌣ x)) comm⌣Dep n m x y = toPathP {A = λ i → coHom (+'-comm m n (~ i)) G' A} - (flipTransport (comm⌣ n m x y)) + (flipTransport (comm⌣ n m x y)) \ No newline at end of file diff --git a/Cubical.Cohomology.EilenbergMacLane.Gysin.html b/Cubical.Cohomology.EilenbergMacLane.Gysin.html index 9316f11026..0ada774816 100644 --- a/Cubical.Cohomology.EilenbergMacLane.Gysin.html +++ b/Cubical.Cohomology.EilenbergMacLane.Gysin.html @@ -98,11 +98,11 @@ , subst-EM-0ₖ (+'≡+ i n)) ∘∙ pre-g n i x indexIso₁ : (n i : ℕ) → EMR∙ (i + n) ≃∙ EMR∙ (n + i) - fst (indexIso₁ n i) = substEquiv EMR (+-comm i n) + fst (indexIso₁ n i) = substEquiv EMR (+-comm i n) snd (indexIso₁ n i) = subst-EM-0ₖ (+-comm i n) indexIso₂ : (n i : ℕ) → EMR∙ (n + i) ≃∙ EMR∙ (n +' i) - fst (indexIso₂ n i) = substEquiv EMR (sym (+'≡+ n i)) + fst (indexIso₂ n i) = substEquiv EMR (sym (+'≡+ n i)) snd (indexIso₂ n i) = subst-EM-0ₖ (sym (+'≡+ n i)) -ₖ^-iso : ∀ {ℓ} {G : AbGroup ℓ} {k : ℕ} (n m : ℕ) → Iso (EM G k) (EM G k) @@ -320,10 +320,10 @@ alt-eq : EMR zero ≃ (S₊∙ n →∙ EMR∙ (n +' zero)) alt-eq = compEquiv (HⁿSⁿ-raw≃G-inv R n , isEquiv-HⁿSⁿ-raw≃G-inv R n) (isoToEquiv (pre∘∙equiv - (substEquiv EMR (sym (+'-comm n zero)) , subst-EM-0ₖ _))) + (substEquiv EMR (sym (+'-comm n zero)) , subst-EM-0ₖ _))) pth : g-comm n zero ≡ alt-eq .fst pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _) - (funExt λ x → sym (subst⁻Subst EMR (+'-comm n zero) + (funExt λ x → sym (subst⁻Subst EMR (+'-comm n zero) (gen-HⁿSⁿ-raw R n .fst x ⌣ₖ r)))) g-cute-equiv (suc i) n = g-ind-main n i (g-cute-equiv i n) @@ -335,13 +335,13 @@ help = compEquiv (_ , g-cute-equiv i n) (isoToEquiv (pre∘∙equiv - (substEquiv EMR (sym (+'≡+ i n)) + (substEquiv EMR (sym (+'≡+ i n)) , subst-EM-0ₖ (sym (+'≡+ i n))))) pth : fst help ≡ pre-g n i pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _) (funExt λ y - → subst⁻Subst EMR (+'≡+ i n) + → subst⁻Subst EMR (+'≡+ i n) (r ⌣ₖ gen-HⁿSⁿ-raw R n .fst y))) -- We may use the above to construct the (generalised) Thom @@ -991,8 +991,8 @@ ≡ fst (alt-hom i t) (fst (helpIso i t) .fst x) j*≡ i t f = cong (j* i .fst) - (sym (substSubst⁻ (λ i → coHomRed i RR EP∙) (minusPath i t) f)) - ∙ sym (substCommSlice (λ i → coHomRed i RR EP∙) + (sym (substSubst⁻ (λ i → coHomRed i RR EP∙) (minusPath i t) f)) + ∙ sym (substCommSlice (λ i → coHomRed i RR EP∙) (λ i → coHom i RR (fst B)) (λ i → j* i .fst) (minusPath i t) (subst (λ i → coHomRed i RR EP∙) (sym (minusPath i t)) f)) ∙ cong (subst (λ i → coHom i RR (fst B)) (minusPath i t)) diff --git a/Cubical.Cohomology.EilenbergMacLane.RingStructure.html b/Cubical.Cohomology.EilenbergMacLane.RingStructure.html index a0fbb3db7f..69ed6beca2 100644 --- a/Cubical.Cohomology.EilenbergMacLane.RingStructure.html +++ b/Cubical.Cohomology.EilenbergMacLane.RingStructure.html @@ -54,7 +54,7 @@ _⌣_ (λ {k} {l} → 0ₕ-⌣ k l) (λ {k} {l} → ⌣-0ₕ k l) - (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-assoc _ _ _) , flipTransport (assoc⌣ _ _ _ _ _ _)))) + (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-assoc _ _ _) , flipTransport (assoc⌣ _ _ _ _ _ _)))) (λ {n} a → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (⌣-1ₕ _ _ ∙ cong (λ p → subst (λ p → coHom p R-ab A) p a) (isSetℕ _ _ _ _))))) diff --git a/Cubical.Data.Bool.Properties.html b/Cubical.Data.Bool.Properties.html index c3f15f7f22..41d4b087fb 100644 --- a/Cubical.Data.Bool.Properties.html +++ b/Cubical.Data.Bool.Properties.html @@ -183,14 +183,14 @@ ⊕-Path x = involPath {f = x ⊕_} (⊕-invol x) ⊕-Path-refl : ⊕-Path false ≡ refl -⊕-Path-refl = isInjectiveTransport refl +⊕-Path-refl = isInjectiveTransport refl ¬transportNot : ∀(P : Bool ≡ Bool) b → ¬ (transport P (not b) ≡ transport P b) ¬transportNot P b eq = not≢const b sub where sub : not b ≡ b sub = subst {A = Bool → Bool} (λ f → f (not b) ≡ f b) - (λ i c → transport⁻Transport P c i) (cong (transport⁻ P) eq) + (λ i c → transport⁻Transport P c i) (cong (transport⁻ P) eq) module BoolReflection where data Table (A : Type₀) (P : Bool ≡ A) : Type₀ where @@ -228,10 +228,10 @@ = Empty.rec (¬transportNot P false (q ∙ sym p)) ⊕-complete : ∀ P → P ≡ ⊕-Path (transport P false) - ⊕-complete P = isInjectiveTransport (categorize P) + ⊕-complete P = isInjectiveTransport (categorize P) ⊕-comp : ∀ p q → ⊕-Path p ∙ ⊕-Path q ≡ ⊕-Path (q ⊕ p) - ⊕-comp p q = isInjectiveTransport (λ i x → ⊕-assoc q p x i) + ⊕-comp p q = isInjectiveTransport (λ i x → ⊕-assoc q p x i) open Iso diff --git a/Cubical.Data.Equality.Univalence.html b/Cubical.Data.Equality.Univalence.html index 1098b2c731..f46419f5ed 100644 --- a/Cubical.Data.Equality.Univalence.html +++ b/Cubical.Data.Equality.Univalence.html @@ -24,7 +24,7 @@ open import Cubical.Foundations.Univalence using () renaming ( ua to uaPath - ; uaβ to uaPathβ + ; uaβ to uaPathβ ; uaIdEquiv to uaIdEquivPath ) diff --git a/Cubical.Data.Fin.Properties.html b/Cubical.Data.Fin.Properties.html index 5c6b65b6ef..abcc607426 100644 --- a/Cubical.Data.Fin.Properties.html +++ b/Cubical.Data.Fin.Properties.html @@ -223,7 +223,7 @@ lemma₅ : ∀ k n (R : Residue k n) → extract R ≡ extract (transport (Residue≡ k n) R) - lemma₅ k n = sym ∘ cong extract ∘ uaβ (Residue≃ k n) + lemma₅ k n = sym ∘ cong extract ∘ uaβ (Residue≃ k n) -- The residue of n modulo k is the same as the residue of k + n. extract≡ : ∀ k n → extract (reduce k n) ≡ extract (reduce k (suc k + n)) @@ -372,7 +372,7 @@ f′ = subst (λ h → Fin h → Fin m) (sym sm≡n) f f′≡f : PathP (λ i → Fin (sm≡n i) → Fin m) f′ f - f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) (sym sm≡n)) (~ i) f + f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) (sym sm≡n)) (~ i) f transport-prf : (Σ[ i ∈ Fin (suc m) ] Σ[ j ∈ Fin (suc m) ] (¬ i ≡ j) × (f′ i ≡ f′ j)) @@ -403,7 +403,7 @@ f′ = subst (λ h → Fin h → Fin m) n≡sn′ f f′≡f : PathP (λ i → Fin (n≡sn′ (~ i)) → Fin m) f′ f - f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) n≡sn′) (~ i) f + f′≡f i = transport-fillerExt (cong (λ h → Fin h → Fin m) n≡sn′) (~ i) f transport-prf : (Σ[ i ∈ Fin (suc n′) ] Σ[ j ∈ Fin (suc n′) ] (¬ i ≡ j) × (f′ i ≡ f′ j)) @@ -428,9 +428,9 @@ → transport p x ≡ transport p y → x ≡ y transport-p-inj {x = x} {y = y} {p = p} q = - x ≡⟨ sym (transport⁻Transport p x) ⟩ + x ≡⟨ sym (transport⁻Transport p x) ⟩ transport (sym p) (transport p x) ≡⟨ cong (transport (sym p)) q ⟩ - transport (sym p) (transport p y) ≡⟨ transport⁻Transport p y ⟩ + transport (sym p) (transport p y) ≡⟨ transport⁻Transport p y ⟩ y ∎ Fin-inj : (n m : ℕ) → Fin n ≡ Fin m → n ≡ m diff --git a/Cubical.Data.Fin.Recursive.Properties.html b/Cubical.Data.Fin.Recursive.Properties.html index e2ead24b1f..9d0c937736 100644 --- a/Cubical.Data.Fin.Recursive.Properties.html +++ b/Cubical.Data.Fin.Recursive.Properties.html @@ -217,8 +217,8 @@ ... | i , j , i#j , p = #→≢ i#j i≡j where i≡j : i ≡ j - i≡j = transport (λ k → transport⁻Transport P i k ≡ transport⁻Transport P j k) - (cong (transport⁻ P) p) + i≡j = transport (λ k → transport⁻Transport P i k ≡ transport⁻Transport P j k) + (cong (transport⁻ P) p) Fin-inj : (m n : ℕ) → Fin m ≡ Fin n → m ≡ n Fin-inj m n P with m ≟ n diff --git a/Cubical.Data.FinSet.Binary.Large.html b/Cubical.Data.FinSet.Binary.Large.html index 86f3cd6ae0..bd0a4d2fe6 100644 --- a/Cubical.Data.FinSet.Binary.Large.html +++ b/Cubical.Data.FinSet.Binary.Large.html @@ -133,7 +133,7 @@ PQR : ua PQ ∙ ua QR ≡ ua PR PQR = ua PQ ∙ ua QR - ≡[ i ]⟨ uaCompEquiv PQ QR (~ i) ⟩ + ≡[ i ]⟨ uaCompEquiv PQ QR (~ i) ⟩ ua (compEquiv PQ QR) ≡⟨ cong ua PQRE ⟩ ua PR ∎ diff --git a/Cubical.Data.FinSet.Binary.Small.Properties.html b/Cubical.Data.FinSet.Binary.Small.Properties.html index 2ea5029c97..5ffb1279f3 100644 --- a/Cubical.Data.FinSet.Binary.Small.Properties.html +++ b/Cubical.Data.FinSet.Binary.Small.Properties.html @@ -58,7 +58,7 @@ isGroupoidBinary : isGroupoid Binary isGroupoidBinary b c = isOfHLevelRetract 2 fun inv leftInv sub where - open Iso (pathIso b c) + open Iso (pathIso b c) sub : isSet (El b ≡ El c) sub = isOfHLevel≡ 2 (isSetEl b) (isSetEl c) @@ -72,11 +72,11 @@ lemma B = rec Sprp (_,_ ℕ₂) where Fprp : isProp (fiber El B) - Fprp = isEmbedding→hasPropFibers isEmbeddingEl B + Fprp = isEmbedding→hasPropFibers isEmbeddingEl B Sprp : isProp (Σ[ b ∈ Binary ] El b ≃ B) - Sprp = isOfHLevelRetract 1 (map-snd ua) (map-snd pathToEquiv) - (λ{ (A , e) → ΣPathP (refl , pathToEquiv-ua e) }) Fprp + Sprp = isOfHLevelRetract 1 (map-snd ua) (map-snd pathToEquiv) + (λ{ (A , e) → ΣPathP (refl , pathToEquiv-ua e) }) Fprp smaller : FS.Binary ℓ-zero → Binary smaller (B , tp) = lemma B tp .fst @@ -89,7 +89,7 @@ b≡B = ua (lemma B tp .snd) smaller-bigger : ∀ b → smaller (bigger b) ≡ b - smaller-bigger b = equivIso _ _ .inv (lemma (El b) (isBinaryEl b) .snd) + smaller-bigger b = equivIso _ _ .inv (lemma (El b) (isBinaryEl b) .snd) reflectIso : Iso Binary (FS.Binary ℓ-zero) reflectIso .fun = bigger @@ -113,5 +113,5 @@ path = ua (compEquiv (invEquiv LiftEquiv) reflect) bs : FS.BinStructure (Lift Binary) - bs = subst⁻ FS.BinStructure path FS.structure₀ + bs = subst⁻ FS.BinStructure path FS.structure₀ \ No newline at end of file diff --git a/Cubical.Data.FinSet.Cardinality.html b/Cubical.Data.FinSet.Cardinality.html index 899c55a852..41d587d736 100644 --- a/Cubical.Data.FinSet.Cardinality.html +++ b/Cubical.Data.FinSet.Cardinality.html @@ -72,7 +72,7 @@ cardInj : card X ≡ card Y → ∥ X .fst ≃ Y .fst ∥₁ cardInj {X = X} {Y = Y} p = - ∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ∣₁ ⋆̂ ∣invEquiv∣ (∣≃card∣ Y) + ∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ∣₁ ⋆̂ ∣invEquiv∣ (∣≃card∣ Y) cardReflection : card X ≡ n → ∥ X .fst ≃ Fin n ∥₁ cardReflection {X = X} = cardInj {X = X} {Y = _ , isFinSetFin} @@ -106,7 +106,7 @@ card≡1→isContr : card X ≡ 1 → isContr (X .fst) card≡1→isContr p = Prop.rec isPropIsContr - (λ e → isOfHLevelRespectEquiv 0 (invEquiv (e ⋆ substEquiv Fin p)) isContrSumFin1) (∣≃card∣ X) + (λ e → isOfHLevelRespectEquiv 0 (invEquiv (e ⋆ substEquiv Fin p)) isContrSumFin1) (∣≃card∣ X) card≤1→isProp : card X ≤ 1 → isProp (X .fst) card≤1→isProp p = @@ -120,7 +120,7 @@ ua e i , isProp→PathP {B = λ j → isFinSet (ua e j)} (λ _ → isPropIsFinSet) (X .snd) (𝔽in n .snd) i )) - (∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ⋆ invEquiv (𝔽in≃Fin n) ∣₁) + (∣≃card∣ X ⋆̂ ∣ pathToEquiv (cong Fin p) ⋆ invEquiv (𝔽in≃Fin n) ∣₁) card≡0 : card X ≡ 0 → X ≡ 𝟘 card≡0 p = @@ -627,7 +627,7 @@ isFinSet≃Eff' (yes p) = factorial (card Y) , Prop.elim2 (λ _ _ → isPropPropTrunc {A = _ ≃ Fin _}) (λ p1 p2 - → ∣ equivComp (p1 ⋆ pathToEquiv (cong Fin p) ⋆ SumFin≃Fin _) (p2 ⋆ SumFin≃Fin _) + → ∣ equivComp (p1 ⋆ pathToEquiv (cong Fin p) ⋆ SumFin≃Fin _) (p2 ⋆ SumFin≃Fin _) ⋆ lehmerEquiv ⋆ lehmerFinEquiv ⋆ invEquiv (SumFin≃Fin _) ∣₁) (∣≃card∣ X) (∣≃card∣ Y) @@ -640,5 +640,5 @@ (X Y : FinSet ℓ) where isFinSetType≡Eff : isFinSet (X .fst ≡ Y .fst) - isFinSetType≡Eff = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃Eff X Y) + isFinSetType≡Eff = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃Eff X Y) \ No newline at end of file diff --git a/Cubical.Data.FinSet.Constructors.html b/Cubical.Data.FinSet.Constructors.html index 61fed892dc..d76b161446 100644 --- a/Cubical.Data.FinSet.Constructors.html +++ b/Cubical.Data.FinSet.Constructors.html @@ -163,7 +163,7 @@ (X Y : FinSet ℓ ) where isFinSetType≡ : isFinSet (X .fst ≡ Y .fst) - isFinSetType≡ = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃ X Y) + isFinSetType≡ = EquivPresIsFinSet (invEquiv univalence) (isFinSet≃ X Y) module _ (X : FinSet ℓ) where @@ -173,7 +173,7 @@ Prop.map (λ p → isFinOrd≃ (X .fst) (card X , p) .snd) (X .snd .snd) isFinSetTypeAut : isFinSet (X .fst ≡ X .fst) - isFinSetTypeAut = EquivPresIsFinSet (invEquiv univalence) isFinSetAut + isFinSetTypeAut = EquivPresIsFinSet (invEquiv univalence) isFinSetAut module _ (X : FinSet ℓ) where diff --git a/Cubical.Data.FinSet.Properties.html b/Cubical.Data.FinSet.Properties.html index 8293c665fb..bb3dcbd31b 100644 --- a/Cubical.Data.FinSet.Properties.html +++ b/Cubical.Data.FinSet.Properties.html @@ -94,5 +94,5 @@ transpFamily : {A : Type ℓ}{B : A → Type ℓ'} → ((n , e) : isFinOrd A) → (x : A) → B x ≃ B (invEq e (e .fst x)) -transpFamily {B = B} (n , e) x = pathToEquiv (λ i → B (retEq e x (~ i))) +transpFamily {B = B} (n , e) x = pathToEquiv (λ i → B (retEq e x (~ i))) \ No newline at end of file diff --git a/Cubical.Data.FinSet.Quotients.html b/Cubical.Data.FinSet.Quotients.html index c2f74c74e3..07ce6c1dc6 100644 --- a/Cubical.Data.FinSet.Quotients.html +++ b/Cubical.Data.FinSet.Quotients.html @@ -107,7 +107,7 @@ → ((a : X .fst) → f a ≡ dec a x .fst) → (a : X .fst) → Bool→Type* {ℓ = ℓ'} (f a) ≃ ∥ R a x ∥₁ isEqClassEff→isEqClass' f x h a = - pathToEquiv (cong Bool→Type* (h a)) + pathToEquiv (cong Bool→Type* (h a)) ⋆ invEquiv (LiftDecProp (dec a x)) ⋆ invEquiv (propTruncIdempotent≃ (isDecProp→isProp (dec a x))) diff --git a/Cubical.Data.Int.MoreInts.QuoInt.Base.html b/Cubical.Data.Int.MoreInts.QuoInt.Base.html index c7076e7226..5fed065bbf 100644 --- a/Cubical.Data.Int.MoreInts.QuoInt.Base.html +++ b/Cubical.Data.Int.MoreInts.QuoInt.Base.html @@ -184,9 +184,9 @@ addℤ (posneg _) n = n isEquivAddℤ : (m : ℤ) → isEquiv (addℤ m) -isEquivAddℤ (pos n) = isEquivTransport (addEqℤ n) -isEquivAddℤ (neg n) = isEquivTransport (subEqℤ n) -isEquivAddℤ (posneg _) = isEquivTransport refl +isEquivAddℤ (pos n) = isEquivTransport (addEqℤ n) +isEquivAddℤ (neg n) = isEquivTransport (subEqℤ n) +isEquivAddℤ (posneg _) = isEquivTransport refl addℤ≡+ℤ : addℤ ≡ _+_ addℤ≡+ℤ i (pos (suc m)) n = sucℤ (addℤ≡+ℤ i (pos m) n) diff --git a/Cubical.Data.Int.Properties.html b/Cubical.Data.Int.Properties.html index 5fbbce0e11..fb61a8b93c 100644 --- a/Cubical.Data.Int.Properties.html +++ b/Cubical.Data.Int.Properties.html @@ -589,8 +589,8 @@ -- compPath (λ i → (+'≡+ i (predℤ m) (negsuc n))) (sym (predℤ+negsuc n m)) i isEquivAddℤ' : (m : ℤ) → isEquiv (λ n → n +' m) -isEquivAddℤ' (pos n) = isEquivTransport (addEq n) -isEquivAddℤ' (negsuc n) = isEquivTransport (subEq (suc n)) +isEquivAddℤ' (pos n) = isEquivTransport (addEq n) +isEquivAddℤ' (negsuc n) = isEquivTransport (subEq (suc n)) isEquivAddℤ : (m : ℤ) → isEquiv (λ n → n + m) isEquivAddℤ = subst (λ add → (m : ℤ) → isEquiv (λ n → add n m)) +'≡+ isEquivAddℤ' diff --git a/Cubical.Data.List.Dependent.html b/Cubical.Data.List.Dependent.html index e0cc25e5bf..e1bf40d528 100644 --- a/Cubical.Data.List.Dependent.html +++ b/Cubical.Data.List.Dependent.html @@ -64,7 +64,7 @@ → {as : List A} → isOfHLevel (suc (suc n)) (ListP B as) isOfHLevelSucSuc-ListP n {A} {B} isHB {as} = - subst⁻ (isOfHLevel (suc (suc n))) (pathRepListP B as) (isOfHLevelSucSuc-RepListP n isHB as) + subst⁻ (isOfHLevel (suc (suc n))) (pathRepListP B as) (isOfHLevelSucSuc-RepListP n isHB as) -------------------------- diff --git a/Cubical.Data.Nat.Algebra.html b/Cubical.Data.Nat.Algebra.html index d5b950f2c7..1b3adcf10c 100644 --- a/Cubical.Data.Nat.Algebra.html +++ b/Cubical.Data.Nat.Algebra.html @@ -218,11 +218,11 @@ P (N .alg-suc n) ! α-h (N .alg-suc n) ≡[ i ]⟨ P-suc n i ! α-h _ ⟩ Q-suc n ! α-h (N .alg-suc n) - ≡⟨ substComposite (F .Fiber) (σ n) (cong (N .alg-suc) (P n)) _ ⟩ + ≡⟨ substComposite (F .Fiber) (σ n) (cong (N .alg-suc) (P n)) _ ⟩ cong (N .alg-suc) (P n) ! (σ n ! α-h (N .alg-suc n)) ≡[ i ]⟨ cong (N .alg-suc) (P n) ! fromPathP (σ-h n) i ⟩ cong (N .alg-suc) (P n) ! (F .fib-suc (α-h n)) - ≡⟨ substCommSlice (F .Fiber) (F .Fiber ∘ N .alg-suc) (λ _ → F .fib-suc) (P n) (α-h n) ⟩ + ≡⟨ substCommSlice (F .Fiber) (F .Fiber ∘ N .alg-suc) (λ _ → F .fib-suc) (P n) (α-h n) ⟩ F .fib-suc (P n ! α-h n) ∎ diff --git a/Cubical.Data.Nat.Lower.html b/Cubical.Data.Nat.Lower.html index 1ef3e5fedf..d1f22e53db 100644 --- a/Cubical.Data.Nat.Lower.html +++ b/Cubical.Data.Nat.Lower.html @@ -250,7 +250,7 @@ isInjectiveLower : Lower m ≡ Lower n → m ≡ n isInjectiveLower {m} {n} P = curry ΣPathP - (lemma (m .fst) (n .fst) (m .snd) (n .snd) (pathToIso P)) + (lemma (m .fst) (n .fst) (m .snd) (n .snd) (pathToIso P)) (isPropDepIsMonotone (m .snd) (n .snd) _) where lemma diff --git a/Cubical.Data.Nat.Order.Recursive.html b/Cubical.Data.Nat.Order.Recursive.html index ba72eb6c10..b244adf4c7 100644 --- a/Cubical.Data.Nat.Order.Recursive.html +++ b/Cubical.Data.Nat.Order.Recursive.html @@ -134,7 +134,7 @@ wf-rec-< (suc n) m m≤n with ≤-split {m} {n} m≤n ... | inl m<n = wf-rec-< n m m<n - ... | inr m≡n = subst⁻ (Acc _<_) m≡n (wf-< n) + ... | inr m≡n = subst⁻ (Acc _<_) m≡n (wf-< n) wf-elim : (∀ n → (∀ m → m < n → P m) → P n) → ∀ n → P n wf-elim = WFI.induction WellFounded.wf-< @@ -164,7 +164,7 @@ ... | no ¬Pn = inr λ m m≤n → case ≤-split m≤n of λ where (inl m<n) → ¬P<n m m<n - (inr m≡n) → subst⁻ (¬_ ∘ P) m≡n ¬Pn + (inr m≡n) → subst⁻ (¬_ ∘ P) m≡n ¬Pn →Least : (∀ m → Dec (P m)) → Σ _ P → Σ _ (Least P) →Least dec (n , Pn) with search dec n diff --git a/Cubical.Data.Nat.Properties.html b/Cubical.Data.Nat.Properties.html index d32fe4ad6f..6db4d268f4 100644 --- a/Cubical.Data.Nat.Properties.html +++ b/Cubical.Data.Nat.Properties.html @@ -339,6 +339,6 @@ → subst A q (subst A p x) ≡ subst A r x compSubstℕ {A = A} p q r {x = x} = - sym (substComposite A p q x) + sym (substComposite A p q x) ∙ λ i → subst A (isSetℕ _ _ (p ∙ q) r i) x \ No newline at end of file diff --git a/Cubical.Data.Sigma.Properties.html b/Cubical.Data.Sigma.Properties.html index 792f13534c..afdef3c9f1 100644 --- a/Cubical.Data.Sigma.Properties.html +++ b/Cubical.Data.Sigma.Properties.html @@ -190,7 +190,7 @@ where ε = isHAEquiv.rinv (snd (iso→HAEquiv isom)) goal : subst B (ε x) (subst B (sym (ε x)) y) ≡ y - goal = sym (substComposite B (sym (ε x)) (ε x) y) + goal = sym (substComposite B (sym (ε x)) (ε x) y) ∙∙ cong (λ x → subst B x y) (lCancel (ε x)) ∙∙ substRefl {B = B} y leftInv (Σ-cong-iso-fst {A = A} {B = B} isom) (x , y) = ΣPathP (leftInv isom x , toPathP goal) @@ -202,7 +202,7 @@ lem x = cong (λ a → sym (ε (fun isom x)) ∙ a) (γ x) ∙ lCancel (ε (fun isom x)) goal : subst B (cong (fun isom) (leftInv isom x)) (subst B (sym (ε (fun isom x))) y) ≡ y - goal = sym (substComposite B (sym (ε (fun isom x))) (cong (fun isom) (leftInv isom x)) y) + goal = sym (substComposite B (sym (ε (fun isom x))) (cong (fun isom) (leftInv isom x)) y) ∙∙ cong (λ a → subst B a y) (lem x) ∙∙ substRefl {B = B} y diff --git a/Cubical.Data.SumFin.Properties.html b/Cubical.Data.SumFin.Properties.html index c1b27c292f..b0064920e2 100644 --- a/Cubical.Data.SumFin.Properties.html +++ b/Cubical.Data.SumFin.Properties.html @@ -80,7 +80,7 @@ ⋆ SumFin⊎≃ (f (inl tt)) (totalSum (λ x → f (inr x))) SumFin×≃ : (m n : ℕ) → (Fin m × Fin n) ≃ (Fin (m · n)) -SumFin×≃ m n = SumFinΣ≃ m (λ _ → n) ⋆ pathToEquiv (λ i → Fin (totalSumConst {m = m} n i)) +SumFin×≃ m n = SumFinΣ≃ m (λ _ → n) ⋆ pathToEquiv (λ i → Fin (totalSumConst {m = m} n i)) SumFinΠ≃ : (n : ℕ)(f : Fin n → ℕ) → ((x : Fin n) → Fin (f x)) ≃ (Fin (totalProd f)) SumFinΠ≃ 0 _ = isContr→≃Unit (isContrΠ⊥) ⋆ invEquiv (⊎-IdR-⊥-≃) diff --git a/Cubical.Displayed.Base.html b/Cubical.Displayed.Base.html index e045def5da..3c1517647b 100644 --- a/Cubical.Displayed.Base.html +++ b/Cubical.Displayed.Base.html @@ -63,7 +63,7 @@ uaᴰρ {a} b b' = compEquiv (uaᴰ b (ρ _) b') - (substEquiv (λ q → PathP (λ i → B (q i)) b b') (secEq (ua a a) refl)) + (substEquiv (λ q → PathP (λ i → B (q i)) b b') (secEq (ua a a) refl)) ρᴰ : {a : A} → (b : B a) → b ≅ᴰ⟨ ρ a ⟩ b ρᴰ {a} b = invEq (uaᴰρ b b) refl diff --git a/Cubical.Displayed.Generic.html b/Cubical.Displayed.Generic.html index d9ae547aca..a159aa1363 100644 --- a/Cubical.Displayed.Generic.html +++ b/Cubical.Displayed.Generic.html @@ -33,6 +33,6 @@ -- SubstRel for an arbitrary family 𝒮ˢ-generic : {A : Type ℓA} (𝒮-A : UARel A ℓ≅A) (B : A → Type ℓB) → SubstRel 𝒮-A B -𝒮ˢ-generic 𝒮-A B .SubstRel.act p = substEquiv B (UARel.≅→≡ 𝒮-A p) +𝒮ˢ-generic 𝒮-A B .SubstRel.act p = substEquiv B (UARel.≅→≡ 𝒮-A p) 𝒮ˢ-generic 𝒮-A B .SubstRel.uaˢ p b = refl \ No newline at end of file diff --git a/Cubical.Displayed.Morphism.html b/Cubical.Displayed.Morphism.html index f90159bf4b..e6a8453fca 100644 --- a/Cubical.Displayed.Morphism.html +++ b/Cubical.Displayed.Morphism.html @@ -56,7 +56,7 @@ 𝒮ᴰ-reindex {C = C} f 𝒮ᴰ-C .DUARel.uaᴰ c p c' = compEquiv (𝒮ᴰ-C .DUARel.uaᴰ c (f .rel p) c') - (substEquiv (λ q → PathP (λ i → C (q i)) c c') (sym (f .ua p))) + (substEquiv (λ q → PathP (λ i → C (q i)) c c') (sym (f .ua p))) 𝒮ˢ-reindex : {A : Type ℓA} {𝒮-A : UARel A ℓ≅A} {B : Type ℓB} {𝒮-B : UARel B ℓ≅B} {C : B → Type ℓC} (f : UARelHom 𝒮-A 𝒮-B) diff --git a/Cubical.Displayed.Properties.html b/Cubical.Displayed.Properties.html index 84ac5fa068..2d39c4de31 100644 --- a/Cubical.Displayed.Properties.html +++ b/Cubical.Displayed.Properties.html @@ -6,7 +6,7 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Univalence using (pathToEquiv; univalence; ua-ungluePath-Equiv) +open import Cubical.Foundations.Univalence using (pathToEquiv; univalence; ua-ungluePath-Equiv) open import Cubical.Data.Unit open import Cubical.Data.Sigma @@ -72,7 +72,7 @@ (sym (Iso.rightInv (uaIso a a) refl)) refl uni' : (b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ PathP (λ i → B (≅→≡ (ρ a) i)) b b' - uni' b' = compEquiv (uni b b') (pathToEquiv (g b')) + uni' b' = compEquiv (uni b b') (pathToEquiv (g b')) 𝒮ᴰ-make-1 : (uni : {a : A} (b b' : B a) → b ≅ᴰ⟨ ρ a ⟩ b' ≃ (b ≡ b')) → DUARel 𝒮-A B ℓ≅B diff --git a/Cubical.Displayed.Subst.html b/Cubical.Displayed.Subst.html index 5c104a882d..3792aa863a 100644 --- a/Cubical.Displayed.Subst.html +++ b/Cubical.Displayed.Subst.html @@ -42,7 +42,7 @@ subst B (sym (≅→≡ p)) (equivFun (act p) (invEq (act p) b)) ≡⟨ cong (subst B (sym (≅→≡ p))) (sym (uaˢ p (invEq (act p) b))) ⟩ subst B (sym (≅→≡ p)) (subst B (≅→≡ p) (invEq (act p) b)) - ≡⟨ pathToIso (cong B (≅→≡ p)) .Iso.leftInv (invEq (act p) b) ⟩ + ≡⟨ pathToIso (cong B (≅→≡ p)) .Iso.leftInv (invEq (act p) b) ⟩ invEq (act p) b ∎ diff --git a/Cubical.Displayed.Universe.html b/Cubical.Displayed.Universe.html index dd0b96f656..6823ab9484 100644 --- a/Cubical.Displayed.Universe.html +++ b/Cubical.Displayed.Universe.html @@ -22,11 +22,11 @@ 𝒮-Univ : ∀ ℓ → UARel (Type ℓ) ℓ 𝒮-Univ ℓ .UARel._≅_ = _≃_ -𝒮-Univ ℓ .UARel.ua _ _ = isoToEquiv (invIso univalenceIso) +𝒮-Univ ℓ .UARel.ua _ _ = isoToEquiv (invIso univalenceIso) 𝒮ˢ-El : ∀ ℓ → SubstRel (𝒮-Univ ℓ) (λ X → X) 𝒮ˢ-El ℓ .SubstRel.act e = e -𝒮ˢ-El ℓ .SubstRel.uaˢ e a = uaβ e a +𝒮ˢ-El ℓ .SubstRel.uaˢ e a = uaβ e a 𝒮ᴰ-El : ∀ ℓ → DUARel (𝒮-Univ ℓ) (λ X → X) ℓ 𝒮ᴰ-El ℓ .DUARel._≅ᴰ⟨_⟩_ a e a' = e .fst a ≡ a' diff --git a/Cubical.Experiments.EscardoSIP.html b/Cubical.Experiments.EscardoSIP.html index a92f07f36a..2fbc1d68e9 100644 --- a/Cubical.Experiments.EscardoSIP.html +++ b/Cubical.Experiments.EscardoSIP.html @@ -99,7 +99,7 @@ φψ : (z : (Σ Y A)) → φ (ψ z) ≡ z φψ (y , a) = - ΣPathTransport→PathΣ _ _ (η y , transportTransport⁻ (λ i → A (η y i)) a) + ΣPathTransport→PathΣ _ _ (η y , transportTransport⁻ (λ i → A (η y i)) a) -- last term proves transp (λ i → A (η y i)) i0 (transp (λ i → A (η y (~ i))) i0 a) ≡ a ψφ : (z : (Σ X (A ∘ f))) → ψ (φ z) ≡ z @@ -110,7 +110,7 @@ q : transp (λ i → A (f (ε x i))) i0 (transp (λ i → A (η (f x) (~ i))) i0 a) ≡ a q = transp (λ i → A (f (ε x i))) i0 b ≡⟨ i ⟩ - transp (λ i → A (η (f x) i)) i0 b ≡⟨ transportTransport⁻ (λ i → A (η (f x) i)) a ⟩ + transp (λ i → A (η (f x) i)) i0 b ≡⟨ transportTransport⁻ (λ i → A (η (f x) i)) a ⟩ a ∎ where i : (transp (λ i → A (f (ε x i))) i0 b) ≡ (transp (λ i → A (η (f x) i)) i0 b) @@ -160,19 +160,19 @@ hom-lemma-dep : (S : Type ℓ → Type ℓ') (ι : StrEquiv S ℓ'') (θ : SNS S ι) → (A B : TypeWithStr ℓ S) → (p : (typ A) ≡ (typ B)) - → (PathP (λ i → S (p i)) (str A) (str B)) ≃ (ι A B (pathToEquiv p)) + → (PathP (λ i → S (p i)) (str A) (str B)) ≃ (ι A B (pathToEquiv p)) hom-lemma-dep S ι θ A B p = (J P (λ s → γ s) p) (str B) where - P = (λ y x → (s : S y) → PathP (λ i → S (x i)) (str A) s ≃ ι A (y , s) (pathToEquiv x)) + P = (λ y x → (s : S y) → PathP (λ i → S (x i)) (str A) s ≃ ι A (y , s) (pathToEquiv x)) - γ : (s : S (typ A)) → ((str A) ≡ s) ≃ ι A ((typ A) , s) (pathToEquiv refl) - γ s = subst (λ f → ((str A) ≡ s) ≃ ι A ((typ A) , s) f) (sym pathToEquivRefl) (θ (str A) s) + γ : (s : S (typ A)) → ((str A) ≡ s) ≃ ι A ((typ A) , s) (pathToEquiv refl) + γ s = subst (λ f → ((str A) ≡ s) ≃ ι A ((typ A) , s) f) (sym pathToEquivRefl) (θ (str A) s) -- Define the inverse of Id→homEq directly. -ua-lemma : (A B : Type ℓ) (e : A ≃ B) → (pathToEquiv (ua e)) ≡ e -ua-lemma A B e = EquivJ (λ A f → (pathToEquiv (ua f)) ≡ f) - (subst (λ r → pathToEquiv r ≡ idEquiv B) (sym uaIdEquiv) pathToEquivRefl) +ua-lemma : (A B : Type ℓ) (e : A ≃ B) → (pathToEquiv (ua e)) ≡ e +ua-lemma A B e = EquivJ (λ A f → (pathToEquiv (ua f)) ≡ f) + (subst (λ r → pathToEquiv r ≡ idEquiv B) (sym uaIdEquiv) pathToEquivRefl) e @@ -182,7 +182,7 @@ where p = ua f - ψ : ι A B (pathToEquiv p) + ψ : ι A B (pathToEquiv p) ψ = subst (λ g → ι A B g) (sym (ua-lemma (typ A) (typ B) f)) φ q : PathP (λ i → S (p i)) (str A) (str B) @@ -195,12 +195,12 @@ SIP S ι θ A B = (A ≡ B) ≃⟨ i ⟩ (Σ[ p ∈ (typ A) ≡ (typ B) ] PathP (λ i → S (p i)) (str A) (str B)) ≃⟨ ii ⟩ - (Σ[ p ∈ (typ A) ≡ (typ B) ] (ι A B (pathToEquiv p))) ≃⟨ iii ⟩ + (Σ[ p ∈ (typ A) ≡ (typ B) ] (ι A B (pathToEquiv p))) ≃⟨ iii ⟩ (A ≃[ ι ] B) ■ where i = invEquiv ΣPath≃PathΣ ii = Σ-cong-≃ (hom-lemma-dep S ι θ A B) - iii = Σ-change-of-variable-≃ pathToEquiv (equivIsEquiv univalence) + iii = Σ-change-of-variable-≃ pathToEquiv (equivIsEquiv univalence) diff --git a/Cubical.Experiments.FunExtFromUA.html b/Cubical.Experiments.FunExtFromUA.html index c669a894f8..a75a2fb741 100644 --- a/Cubical.Experiments.FunExtFromUA.html +++ b/Cubical.Experiments.FunExtFromUA.html @@ -23,7 +23,7 @@ pre-comp-is-equiv : (X Y : Type ℓ) (f : X → Y) (Z : Type ℓ) → isEquiv f → isEquiv (λ (g : Y → Z) → g ∘ f) -pre-comp-is-equiv {ℓ} X Y f Z e = elimEquivFun P r (f , e) +pre-comp-is-equiv {ℓ} X Y f Z e = elimEquivFun P r (f , e) where P : (X : Type ℓ) → (X → Y) → Type ℓ P X f = isEquiv (λ (g : Y → Z) → g ∘ f) diff --git a/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html b/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html index 69cab89e75..7855cb4d92 100644 --- a/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html +++ b/Cubical.Experiments.ZCohomologyOld.KcompPrelims.html @@ -171,7 +171,7 @@ d-map p = subst HopfSuspS¹ p base d-mapId : (r : S¹) → d-map (ϕ base r) ≡ r - d-mapId r = substComposite HopfSuspS¹ (merid r) (sym (merid base)) base ∙ + d-mapId r = substComposite HopfSuspS¹ (merid r) (sym (merid base)) base ∙ rotLemma r where rotLemma : (r : S¹) → r · base ≡ r diff --git a/Cubical.Foundations.CartesianKanOps.html b/Cubical.Foundations.CartesianKanOps.html index 02151b7631..a61daca77e 100644 --- a/Cubical.Foundations.CartesianKanOps.html +++ b/Cubical.Foundations.CartesianKanOps.html @@ -90,7 +90,7 @@ { (i = i0) → a ; (i = i1) → coe1→i A (j ∨ k) a ; (j = i1) → a }) - (transpFill {A = A i0} (~ i) (λ t → inS (A (i ∧ ~ t))) a (~ j)) + (transpFill {A = A i0} (~ i) (λ t → inS (A (i ∧ ~ t))) a (~ j)) coe0→0 : ∀ {ℓ} (A : I → Type ℓ) (a : A i0) → coei→i A i0 a ≡ refl coe0→0 A a = refl diff --git a/Cubical.Foundations.Equiv.Base.html b/Cubical.Foundations.Equiv.Base.html index ec269e7667..24b1497fb9 100644 --- a/Cubical.Foundations.Equiv.Base.html +++ b/Cubical.Foundations.Equiv.Base.html @@ -30,4 +30,38 @@ -- the definition using Π-type isEquiv' : ∀ {ℓ}{ℓ'}{A : Type ℓ}{B : Type ℓ'} → (A → B) → Type (ℓ-max ℓ ℓ') isEquiv' {B = B} f = (y : B) → isContr (fiber f y) + +-- Transport along a line of types A, constant on some extent φ, is an equivalence. +isEquivTransp : ∀ {ℓ : I → Level} (A : (i : I) → Type (ℓ i)) → ∀ (φ : I) → isEquiv (transp (λ j → A (φ ∨ j)) φ) +isEquivTransp A φ = u₁ where + -- NB: The transport in question is the `coei→1` or `squeeze` operation mentioned + -- at `Cubical.Foundations.CartesianKanOps` and + -- https://1lab.dev/1Lab.Path.html#coei%E2%86%921 + coei→1 : A φ → A i1 + coei→1 = transp (λ j → A (φ ∨ j)) φ + + -- A line of types, interpolating between propositions: + -- (k = i0): the identity function is an equivalence + -- (k = i1): transport along A is an equivalence + γ : (k : I) → Type _ + γ k = isEquiv (transp (λ j → A (φ ∨ (j ∧ k))) (φ ∨ ~ k)) + + _ : γ i0 ≡ isEquiv (idfun (A φ)) + _ = refl + + _ : γ i1 ≡ isEquiv coei→1 + _ = refl + + -- We have proof that the identity function *is* an equivalence, + u₀ : γ i0 + u₀ = idIsEquiv (A φ) + + -- and by transporting that evidence along γ, we prove that + -- transporting along A is an equivalence, too. + u₁ : γ i1 + u₁ = transp γ φ u₀ + +transpEquiv : ∀ {ℓ : I → Level} (A : (i : I) → Type (ℓ i)) → ∀ φ → A φ ≃ A i1 +transpEquiv A φ .fst = transp (λ j → A (φ ∨ j)) φ +transpEquiv A φ .snd = isEquivTransp A φ \ No newline at end of file diff --git a/Cubical.Foundations.Equiv.Dependent.html b/Cubical.Foundations.Equiv.Dependent.html index 12f2b69240..340d735c7d 100644 --- a/Cubical.Foundations.Equiv.Dependent.html +++ b/Cubical.Foundations.Equiv.Dependent.html @@ -255,7 +255,7 @@ fibiso a .inv x = transport (λ i → P (isom .leftInv a i)) (isom' .inv (f a) x) fibiso a .leftInv x = fromPathP (isom' .leftInv _ _) fibiso a .rightInv x = - sym (substCommSlice _ _ (isom' .fun) _ _) + sym (substCommSlice _ _ (isom' .fun) _ _) ∙ cong (λ p → subst Q p (isom' .fun _ (isom' .inv _ x))) (hae .com a) ∙ fromPathP (isom' .rightInv _ _) diff --git a/Cubical.Foundations.Equiv.Properties.html b/Cubical.Foundations.Equiv.Properties.html index 1b022cb1ec..c03a336418 100644 --- a/Cubical.Foundations.Equiv.Properties.html +++ b/Cubical.Foundations.Equiv.Properties.html @@ -157,14 +157,14 @@ (g , section-g)) cong≃ : (F : Type ℓ → Type ℓ') → (A ≃ B) → F A ≃ F B -cong≃ F e = pathToEquiv (cong F (ua e)) +cong≃ F e = pathToEquiv (cong F (ua e)) cong≃-char : (F : Type ℓ → Type ℓ') {A B : Type ℓ} (e : A ≃ B) → ua (cong≃ F e) ≡ cong F (ua e) -cong≃-char F e = ua-pathToEquiv (cong F (ua e)) +cong≃-char F e = ua-pathToEquiv (cong F (ua e)) cong≃-idEquiv : (F : Type ℓ → Type ℓ') (A : Type ℓ) → cong≃ F (idEquiv A) ≡ idEquiv (F A) -cong≃-idEquiv F A = cong≃ F (idEquiv A) ≡⟨ cong (λ p → pathToEquiv (cong F p)) uaIdEquiv ⟩ - pathToEquiv refl ≡⟨ pathToEquivRefl ⟩ +cong≃-idEquiv F A = cong≃ F (idEquiv A) ≡⟨ cong (λ p → pathToEquiv (cong F p)) uaIdEquiv ⟩ + pathToEquiv refl ≡⟨ pathToEquivRefl ⟩ idEquiv (F A) ∎ isPropIsHAEquiv : {f : A → B} → isProp (isHAEquiv f) diff --git a/Cubical.Foundations.Everything.html b/Cubical.Foundations.Everything.html index dba18e92db..756d99ddde 100644 --- a/Cubical.Foundations.Everything.html +++ b/Cubical.Foundations.Everything.html @@ -7,29 +7,30 @@ open import Cubical.Foundations.Function public open import Cubical.Foundations.Equiv public -open import Cubical.Foundations.Equiv.Properties public -open import Cubical.Foundations.Equiv.Fiberwise -open import Cubical.Foundations.Equiv.PathSplit public -open import Cubical.Foundations.Equiv.BiInvertible public -open import Cubical.Foundations.Equiv.HalfAdjoint -open import Cubical.Foundations.Equiv.Dependent -open import Cubical.Foundations.HLevels public -open import Cubical.Foundations.HLevels.Extend -open import Cubical.Foundations.Path public -open import Cubical.Foundations.Pointed public -open import Cubical.Foundations.RelationalStructure public -open import Cubical.Foundations.Structure public -open import Cubical.Foundations.Transport public -open import Cubical.Foundations.Univalence public -open import Cubical.Foundations.Univalence.Universe -open import Cubical.Foundations.Univalence.Dependent -open import Cubical.Foundations.GroupoidLaws public -open import Cubical.Foundations.Isomorphism public -open import Cubical.Foundations.CartesianKanOps -open import Cubical.Foundations.Powerset -open import Cubical.Foundations.SIP -open import Cubical.Foundations.Cubes -open import Cubical.Foundations.Cubes.Subtypes -open import Cubical.Foundations.Cubes.Dependent -open import Cubical.Foundations.Cubes.HLevels + hiding (transpEquiv) -- Hide to avoid clash with Transport.transpEquiv +open import Cubical.Foundations.Equiv.Properties public +open import Cubical.Foundations.Equiv.Fiberwise +open import Cubical.Foundations.Equiv.PathSplit public +open import Cubical.Foundations.Equiv.BiInvertible public +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.Equiv.Dependent +open import Cubical.Foundations.HLevels public +open import Cubical.Foundations.HLevels.Extend +open import Cubical.Foundations.Path public +open import Cubical.Foundations.Pointed public +open import Cubical.Foundations.RelationalStructure public +open import Cubical.Foundations.Structure public +open import Cubical.Foundations.Transport public +open import Cubical.Foundations.Univalence public +open import Cubical.Foundations.Univalence.Universe +open import Cubical.Foundations.Univalence.Dependent +open import Cubical.Foundations.GroupoidLaws public +open import Cubical.Foundations.Isomorphism public +open import Cubical.Foundations.CartesianKanOps +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.SIP +open import Cubical.Foundations.Cubes +open import Cubical.Foundations.Cubes.Subtypes +open import Cubical.Foundations.Cubes.Dependent +open import Cubical.Foundations.Cubes.HLevels \ No newline at end of file diff --git a/Cubical.Foundations.HLevels.html b/Cubical.Foundations.HLevels.html index 14f89991ee..ae857ccd32 100644 --- a/Cubical.Foundations.HLevels.html +++ b/Cubical.Foundations.HLevels.html @@ -21,7 +21,7 @@ open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Path open import Cubical.Foundations.Transport -open import Cubical.Foundations.Univalence using (ua ; univalenceIso) +open import Cubical.Foundations.Univalence using (ua ; univalenceIso) open import Cubical.Data.Sigma open import Cubical.Data.Nat using (ℕ; zero; suc; _+_; +-zero; +-comm) @@ -515,7 +515,7 @@ isOfHLevel≡ : ∀ n → {A B : Type ℓ} (hA : isOfHLevel n A) (hB : isOfHLevel n B) → isOfHLevel n (A ≡ B) -isOfHLevel≡ n hA hB = isOfHLevelRetractFromIso n univalenceIso (isOfHLevel≃ n hA hB) +isOfHLevel≡ n hA hB = isOfHLevelRetractFromIso n univalenceIso (isOfHLevel≃ n hA hB) isOfHLevel⁺≃ₗ : ∀ n {A : Type ℓ} {B : Type ℓ'} @@ -547,9 +547,9 @@ isOfHLevel⁺≡ᵣ : ∀ n → {A B : Type ℓ} → isOfHLevel (suc n) B → isOfHLevel (suc n) (A ≡ B) -isOfHLevel⁺≡ᵣ zero pB P = isOfHLevel≡ 1 (subst⁻ isProp P pB) pB P +isOfHLevel⁺≡ᵣ zero pB P = isOfHLevel≡ 1 (subst⁻ isProp P pB) pB P isOfHLevel⁺≡ᵣ (suc n) hB P - = isOfHLevel≡ m (subst⁻ (isOfHLevel m) P hB) hB P + = isOfHLevel≡ m (subst⁻ (isOfHLevel m) P hB) hB P where m = suc (suc n) @@ -793,8 +793,8 @@ ww : Iso _ _ fun ww = isoToPath - inv ww = pathToIso - rightInv ww b = isInjectiveTransport (funExt λ _ → transportRefl _) + inv ww = pathToIso + rightInv ww b = isInjectiveTransport (funExt λ _ → transportRefl _) leftInv ww a = SetsIso≡-ext isSet-A isSet-A' (λ _ → transportRefl (fun a _)) λ _ → cong (inv a) (transportRefl _) hSet-Iso-Iso-≡ : (A : hSet ℓ) → (A' : hSet ℓ) → Iso (Iso (fst A) (fst A')) (A ≡ A') diff --git a/Cubical.Foundations.Path.html b/Cubical.Foundations.Path.html index 9ed5a7ff93..87ee14d45b 100644 --- a/Cubical.Foundations.Path.html +++ b/Cubical.Foundations.Path.html @@ -18,10 +18,10 @@ A : Type ℓ module _ {A : I → Type ℓ} {x : A i0} {y : A i1} where - toPathP⁻ : x ≡ transport⁻ (λ i → A i) y → PathP A x y + toPathP⁻ : x ≡ transport⁻ (λ i → A i) y → PathP A x y toPathP⁻ p = symP (toPathP (sym p)) - fromPathP⁻ : PathP A x y → x ≡ transport⁻ (λ i → A i) y + fromPathP⁻ : PathP A x y → x ≡ transport⁻ (λ i → A i) y fromPathP⁻ p = sym (fromPathP {A = λ i → A (~ i)} (symP p)) PathP≡Path : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) → @@ -29,8 +29,8 @@ PathP≡Path P p q i = PathP (λ j → P (i ∨ j)) (transport-filler (λ j → P j) p i) q PathP≡Path⁻ : ∀ (P : I → Type ℓ) (p : P i0) (q : P i1) → - PathP P p q ≡ Path (P i0) p (transport⁻ (λ i → P i) q) -PathP≡Path⁻ P p q i = PathP (λ j → P (~ i ∧ j)) p (transport⁻-filler (λ j → P j) q i) + PathP P p q ≡ Path (P i0) p (transport⁻ (λ i → P i) q) +PathP≡Path⁻ P p q i = PathP (λ j → P (~ i ∧ j)) p (transport⁻-filler (λ j → P j) q i) PathPIsoPath : ∀ (A : I → Type ℓ) (x : A i0) (y : A i1) → Iso (PathP A x y) (transport (λ i → A i) x ≡ y) PathPIsoPath A x y .Iso.fun = fromPathP @@ -94,7 +94,7 @@ → 3-Constant f 3-Constant.link (3-ConstantCompChar f link coh₂) = link 3-Constant.coh₁ (3-ConstantCompChar f link coh₂) _ _ _ = - transport⁻ (PathP≡compPath _ _ _) (coh₂ _ _ _) + transport⁻ (PathP≡compPath _ _ _) (coh₂ _ _ _) PathP≡doubleCompPathˡ : ∀ {A : Type ℓ} {w x y z : A} (p : w ≡ y) (q : w ≡ x) (r : y ≡ z) (s : x ≡ z) → (PathP (λ i → p i ≡ s i) q r) ≡ (p ⁻¹ ∙∙ q ∙∙ s ≡ r) @@ -197,7 +197,7 @@ (a₀₋ : a₀₀ ≡ a₀₁) (a₁₋ : a₁₀ ≡ a₁₁) (a₋₀ : a₀₀ ≡ a₁₀) (a₋₁ : a₀₁ ≡ a₁₁) → Square a₀₋ a₁₋ a₋₀ a₋₁ ≃ (a₋₀ ⁻¹ ∙∙ a₀₋ ∙∙ a₋₁ ≡ a₁₋) -Square≃doubleComp a₀₋ a₁₋ a₋₀ a₋₁ = pathToEquiv (PathP≡doubleCompPathˡ a₋₀ a₀₋ a₁₋ a₋₁) +Square≃doubleComp a₀₋ a₁₋ a₋₀ a₋₁ = pathToEquiv (PathP≡doubleCompPathˡ a₋₀ a₀₋ a₁₋ a₋₁) -- Flipping a square in Ω²A is the same as inverting it sym≡flipSquare : {x : A} (P : Square (refl {x = x}) refl refl refl) diff --git a/Cubical.Foundations.Pointed.Homotopy.html b/Cubical.Foundations.Pointed.Homotopy.html index 7a4a42a990..292de6d206 100644 --- a/Cubical.Foundations.Pointed.Homotopy.html +++ b/Cubical.Foundations.Pointed.Homotopy.html @@ -95,7 +95,7 @@ -- Proof that ∙∼ and ∙∼P are equivalent using the fiberwise equivalence φ ∙∼≃∙∼P : (f g : Π∙ A B ptB) → (f ∙∼ g) ≃ (f ∙∼P g) - ∙∼≃∙∼P f g = Σ-cong-equiv-snd (λ H → pathToEquiv (P≡Q f g H)) + ∙∼≃∙∼P f g = Σ-cong-equiv-snd (λ H → pathToEquiv (P≡Q f g H)) -- inverse of ∙∼→∙∼P extracted from the equivalence ∙∼P→∙∼ : {f g : Π∙ A B ptB} → f ∙∼P g → f ∙∼ g diff --git a/Cubical.Foundations.SIP.html b/Cubical.Foundations.SIP.html index 2444d29878..bd019a2a4b 100644 --- a/Cubical.Foundations.SIP.html +++ b/Cubical.Foundations.SIP.html @@ -11,7 +11,7 @@ module Cubical.Foundations.SIP where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv') +open import Cubical.Foundations.Univalence renaming (ua-pathToEquiv to ua-pathToEquiv') open import Cubical.Foundations.Transport open import Cubical.Foundations.Function open import Cubical.Foundations.Path @@ -57,7 +57,7 @@ ι (X , s) (X , t) (idEquiv X) ≃⟨ θ (idEquiv X) ⟩ PathP (λ i → S (ua (idEquiv X) i)) s t - ≃⟨ pathToEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = X} j i)) s t) ⟩ + ≃⟨ pathToEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = X} j i)) s t) ⟩ s ≡ t ■ @@ -75,7 +75,7 @@ ι (Y , s) (Y , t) (idEquiv Y) ≃⟨ θ s t ⟩ s ≡ t - ≃⟨ pathToEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = Y} (~ j) i)) s t) ⟩ + ≃⟨ pathToEquiv (λ j → PathP (λ i → S (uaIdEquiv {A = Y} (~ j) i)) s t) ⟩ PathP (λ i → S (ua (idEquiv Y) i)) s t ■ @@ -87,7 +87,7 @@ → TransportStr α → UnivalentStr S (EquivAction→StrEquiv α) TransportStr→UnivalentStr {S = S} α τ {X , s} {Y , t} e = equivFun (α e) s ≡ t - ≃⟨ pathToEquiv (cong (_≡ t) (τ e s)) ⟩ + ≃⟨ pathToEquiv (cong (_≡ t) (τ e s)) ⟩ subst S (ua e) s ≡ t ≃⟨ invEquiv (PathP≃Path _ _ _) ⟩ PathP (λ i → S (ua e i)) s t @@ -99,11 +99,11 @@ invEq (θ e) (transport-filler (cong S (ua e)) s) invTransportStr : {S : Type ℓ → Type ℓ₂} (α : EquivAction S) (τ : TransportStr α) - {X Y : Type ℓ} (e : X ≃ Y) (t : S Y) → invEq (α e) t ≡ subst⁻ S (ua e) t + {X Y : Type ℓ} (e : X ≃ Y) (t : S Y) → invEq (α e) t ≡ subst⁻ S (ua e) t invTransportStr {S = S} α τ e t = - sym (transport⁻Transport (cong S (ua e)) (invEq (α e) t)) - ∙∙ sym (cong (subst⁻ S (ua e)) (τ e (invEq (α e) t))) - ∙∙ cong (subst⁻ S (ua e)) (secEq (α e) t) + sym (transport⁻Transport (cong S (ua e)) (invEq (α e) t)) + ∙∙ sym (cong (subst⁻ S (ua e)) (τ e (invEq (α e) t))) + ∙∙ cong (subst⁻ S (ua e)) (secEq (α e) t) --- We can now define an invertible function @@ -119,7 +119,7 @@ SIP : A ≃[ ι ] B ≃ (A ≡ B) SIP = - sip , isoToIsEquiv (compIso (Σ-cong-iso (invIso univalenceIso) (equivToIso ∘ θ)) ΣPathIsoPathΣ) + sip , isoToIsEquiv (compIso (Σ-cong-iso (invIso univalenceIso) (equivToIso ∘ θ)) ΣPathIsoPathΣ) sip⁻ : A ≡ B → A ≃[ ι ] B sip⁻ = invEq SIP diff --git a/Cubical.Foundations.Transport.html b/Cubical.Foundations.Transport.html index f05b4c28b6..91db5c8f3f 100644 --- a/Cubical.Foundations.Transport.html +++ b/Cubical.Foundations.Transport.html @@ -9,206 +9,201 @@ module Cubical.Foundations.Transport where open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Univalence -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Foundations.Function using (_∘_) - --- Direct definition of transport filler, note that we have to --- explicitly tell Agda that the type is constant (like in CHM) -transpFill : ∀ {ℓ} {A : Type ℓ} - (φ : I) - (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ]) - (u0 : outS (A i0)) - → -------------------------------------- - PathP (λ i → outS (A i)) u0 (transp (λ i → outS (A i)) φ u0) -transpFill φ A u0 i = transp (λ j → outS (A (i ∧ j))) (~ i ∨ φ) u0 - -transport⁻ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A -transport⁻ p = transport (λ i → p (~ i)) - -subst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → B y → B x -subst⁻ B p pa = transport⁻ (λ i → B (p i)) pa - -subst⁻-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) (b : B y) - → PathP (λ i → B (p (~ i))) b (subst⁻ B p b) -subst⁻-filler B p = subst-filler B (sym p) - -transport-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) - → PathP (λ i → A → p i) (λ x → x) (transport p) -transport-fillerExt p i x = transport-filler p x i - -transport⁻-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) - → PathP (λ i → p i → A) (λ x → x) (transport⁻ p) -transport⁻-fillerExt p i x = transp (λ j → p (i ∧ ~ j)) (~ i) x - -transport-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) - → PathP (λ i → p i → B) (transport p) (λ x → x) -transport-fillerExt⁻ p = symP (transport⁻-fillerExt (sym p)) - -transport⁻-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) - → PathP (λ i → B → p i) (transport⁻ p) (λ x → x) -transport⁻-fillerExt⁻ p = symP (transport-fillerExt (sym p)) - - -transport⁻-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : B) - → PathP (λ i → p (~ i)) x (transport⁻ p x) -transport⁻-filler p x = transport-filler (λ i → p (~ i)) x - -transport⁻Transport : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (a : A) → - transport⁻ p (transport p a) ≡ a -transport⁻Transport p a j = transport⁻-fillerExt p (~ j) (transport-fillerExt p (~ j) a) - -transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) → - transport p (transport⁻ p b) ≡ b -transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b) - -subst⁻Subst : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) - → (u : B x) → subst⁻ B p (subst B p u) ≡ u -subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u - -substSubst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) - → (v : B y) → subst B p (subst⁻ B p v) ≡ v -substSubst⁻ {x = x} {y = y} B p v = transportTransport⁻ {A = B x} {B = B y} (cong B p) v - -substEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {a a' : A} (P : A → Type ℓ') (p : a ≡ a') → P a ≃ P a' -substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i))) - -liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A ≃ B) → P A ≃ P B -liftEquiv P e = substEquiv P (ua e) - -transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B -transpEquiv P i .fst = transp (λ j → P (i ∨ j)) i -transpEquiv P i .snd - = transp (λ k → isEquiv (transp (λ j → P (i ∨ (j ∧ k))) (i ∨ ~ k))) - i (idIsEquiv (P i)) - -uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (pathToEquiv P) ≡ P -uaTransportη P i j - = Glue (P i1) λ where - (j = i0) → P i0 , pathToEquiv P - (i = i1) → P j , transpEquiv P j - (j = i1) → P i1 , idEquiv (P i1) - -pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B -Iso.fun (pathToIso x) = transport x -Iso.inv (pathToIso x) = transport⁻ x -Iso.rightInv (pathToIso x) = transportTransport⁻ x -Iso.leftInv (pathToIso x) = transport⁻Transport x - -substIso : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → Iso (B x) (B y) -substIso B p = pathToIso (cong B p) - --- Redefining substEquiv in terms of substIso gives an explicit inverse -substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y -substEquiv' B p = isoToEquiv (substIso B p) - -isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B} - → transport p ≡ transport q → p ≡ q -isInjectiveTransport {p = p} {q} α i = - hcomp - (λ j → λ - { (i = i0) → retEq univalence p j - ; (i = i1) → retEq univalence q j - }) - (invEq univalence ((λ a → α i a) , t i)) - where - t : PathP (λ i → isEquiv (λ a → α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd) - t = isProp→PathP (λ i → isPropIsEquiv (λ a → α i a)) _ _ - -transportUaInv : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → transport (ua (invEquiv e)) ≡ transport (sym (ua e)) -transportUaInv e = cong transport (uaInvEquiv e) --- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give --- refl for the case of idEquiv: --- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e - -isSet-subst : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} - → (isSet-A : isSet A) - → ∀ {a : A} - → (p : a ≡ a) → (x : B a) → subst B p x ≡ x -isSet-subst {B = B} isSet-A p x = subst (λ p′ → subst B p′ x ≡ x) (isSet-A _ _ refl p) (substRefl {B = B} x) - --- substituting along a composite path is equivalent to substituting twice -substComposite : ∀ {ℓ ℓ'} {A : Type ℓ} → (B : A → Type ℓ') - → {x y z : A} (p : x ≡ y) (q : y ≡ z) (u : B x) - → subst B (p ∙ q) u ≡ subst B q (subst B p u) -substComposite B p q Bx i = - transport (cong B (compPath-filler' p q (~ i))) (transport-fillerExt (cong B p) i Bx) - --- transporting along a composite path is equivalent to transporting twice -transportComposite : ∀ {ℓ} {A B C : Type ℓ} (p : A ≡ B) (q : B ≡ C) (x : A) - → transport (p ∙ q) x ≡ transport q (transport p x) -transportComposite = substComposite (λ D → D) - --- substitution commutes with morphisms in slices -substCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} - → (B : A → Type ℓ') (C : A → Type ℓ'') - → (F : ∀ a → B a → C a) - → {x y : A} (p : x ≡ y) (u : B x) - → subst C p (F x u) ≡ F y (subst B p u) -substCommSlice B C F p Bx a = - transport-fillerExt⁻ (cong C p) a (F _ (transport-fillerExt (cong B p) a Bx)) - -constSubstCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} - → (B : A → Type ℓ') - → (C : Type ℓ'') - → (F : ∀ a → B a → C) - → {x y : A} (p : x ≡ y) (u : B x) - → (F x u) ≡ F y (subst B p u) -constSubstCommSlice B C F p Bx = (sym (transportRefl (F _ Bx)) ∙ substCommSlice B (λ _ → C) F p Bx) - --- transporting over (λ i → B (p i) → C (p i)) divides the transport into --- transports over (λ i → C (p i)) and (λ i → B (p (~ i))) -funTypeTransp : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} (B : A → Type ℓ') (C : A → Type ℓ'') {x y : A} (p : x ≡ y) (f : B x → C x) - → PathP (λ i → B (p i) → C (p i)) f (subst C p ∘ f ∘ subst B (sym p)) -funTypeTransp B C {x = x} p f i b = - transp (λ j → C (p (j ∧ i))) (~ i) (f (transp (λ j → B (p (i ∧ ~ j))) (~ i) b)) - --- transports between loop spaces preserve path composition -overPathFunct : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ x) (P : x ≡ y) - → transport (λ i → P i ≡ P i) (p ∙ q) - ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q -overPathFunct p q = - J (λ y P → transport (λ i → P i ≡ P i) (p ∙ q) ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q) - (transportRefl (p ∙ q) ∙ cong₂ _∙_ (sym (transportRefl p)) (sym (transportRefl q))) - --- substition over families of paths --- theorem 2.11.3 in The Book -substInPaths : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {a a' : A} - → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a) - → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p -substInPaths {a = a} f g p q = - J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p')) - p=refl p - where - p=refl : subst (λ y → f y ≡ g y) refl q - ≡ refl ∙ q ∙ refl - p=refl = subst (λ y → f y ≡ g y) refl q - ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q - ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎ - -flipTransport : ∀ {ℓ} {A : I → Type ℓ} {x : A i0} {y : A i1} - → x ≡ transport⁻ (λ i → A i) y - → transport (λ i → A i) x ≡ y -flipTransport {A = A} {y = y} p = - cong (transport (λ i → A i)) p ∙ transportTransport⁻ (λ i → A i) y - --- special cases of substInPaths from lemma 2.11.2 in The Book -module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where - substInPathsL : (q : a ≡ x1) → subst (λ x → a ≡ x) p q ≡ q ∙ p - substInPathsL q = subst (λ x → a ≡ x) p q - ≡⟨ substInPaths (λ _ → a) (λ x → x) p q ⟩ - sym (cong (λ _ → a) p) ∙ q ∙ cong (λ x → x) p - ≡⟨ assoc (λ _ → a) q p ⟩ - (refl ∙ q) ∙ p - ≡⟨ cong (_∙ p) (sym (lUnit q)) ⟩ q ∙ p ∎ - - substInPathsR : (q : x1 ≡ a) → subst (λ x → x ≡ a) p q ≡ sym p ∙ q - substInPathsR q = subst (λ x → x ≡ a) p q - ≡⟨ substInPaths (λ x → x) (λ _ → a) p q ⟩ - sym (cong (λ x → x) p) ∙ q ∙ cong (λ _ → a) p - ≡⟨ assoc (sym p) q refl ⟩ - (sym p ∙ q) ∙ refl - ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ +open import Cubical.Foundations.Equiv as Equiv hiding (transpEquiv) +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Function using (_∘_) + +-- Direct definition of transport filler, note that we have to +-- explicitly tell Agda that the type is constant (like in CHM) +transpFill : ∀ {ℓ} {A : Type ℓ} + (φ : I) + (A : (i : I) → Type ℓ [ φ ↦ (λ _ → A) ]) + (u0 : outS (A i0)) + → -------------------------------------- + PathP (λ i → outS (A i)) u0 (transp (λ i → outS (A i)) φ u0) +transpFill φ A u0 i = transp (λ j → outS (A (i ∧ j))) (~ i ∨ φ) u0 + +transport⁻ : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → B → A +transport⁻ p = transport (λ i → p (~ i)) + +subst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) → B y → B x +subst⁻ B p pa = transport⁻ (λ i → B (p i)) pa + +subst⁻-filler : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) (b : B y) + → PathP (λ i → B (p (~ i))) b (subst⁻ B p b) +subst⁻-filler B p = subst-filler B (sym p) + +transport-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) + → PathP (λ i → A → p i) (λ x → x) (transport p) +transport-fillerExt p i x = transport-filler p x i + +transport⁻-fillerExt : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) + → PathP (λ i → p i → A) (λ x → x) (transport⁻ p) +transport⁻-fillerExt p i x = transp (λ j → p (i ∧ ~ j)) (~ i) x + +transport-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) + → PathP (λ i → p i → B) (transport p) (λ x → x) +transport-fillerExt⁻ p = symP (transport⁻-fillerExt (sym p)) + +transport⁻-fillerExt⁻ : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) + → PathP (λ i → B → p i) (transport⁻ p) (λ x → x) +transport⁻-fillerExt⁻ p = symP (transport-fillerExt (sym p)) + + +transport⁻-filler : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) (x : B) + → PathP (λ i → p (~ i)) x (transport⁻ p x) +transport⁻-filler p x = transport-filler (λ i → p (~ i)) x + +transport⁻Transport : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (a : A) → + transport⁻ p (transport p a) ≡ a +transport⁻Transport p a j = transport⁻-fillerExt p (~ j) (transport-fillerExt p (~ j) a) + +transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B) → + transport p (transport⁻ p b) ≡ b +transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b) + +subst⁻Subst : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) + → (u : B x) → subst⁻ B p (subst B p u) ≡ u +subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u + +substSubst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y) + → (v : B y) → subst B p (subst⁻ B p v) ≡ v +substSubst⁻ {x = x} {y = y} B p v = transportTransport⁻ {A = B x} {B = B y} (cong B p) v + +substEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {a a' : A} (P : A → Type ℓ') (p : a ≡ a') → P a ≃ P a' +substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i))) + +liftEquiv : ∀ {ℓ ℓ'} {A B : Type ℓ} (P : Type ℓ → Type ℓ') (e : A ≃ B) → P A ≃ P B +liftEquiv P e = substEquiv P (ua e) + +transpEquiv : ∀ {ℓ} {A B : Type ℓ} (p : A ≡ B) → ∀ i → p i ≃ B +transpEquiv p = Equiv.transpEquiv (λ i → p i) +{-# WARNING_ON_USAGE transpEquiv "Deprecated: Use the more general `transpEquiv` from `Cubical.Foundations.Equiv` instead" #-} + +uaTransportη : ∀ {ℓ} {A B : Type ℓ} (P : A ≡ B) → ua (pathToEquiv P) ≡ P +uaTransportη = uaη +{-# WARNING_ON_USAGE uaTransportη "Deprecated: Use `uaη` from `Cubical.Foundations.Univalence` instead of `uaTransportη`" #-} + +pathToIso : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → Iso A B +Iso.fun (pathToIso x) = transport x +Iso.inv (pathToIso x) = transport⁻ x +Iso.rightInv (pathToIso x) = transportTransport⁻ x +Iso.leftInv (pathToIso x) = transport⁻Transport x + +substIso : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → Iso (B x) (B y) +substIso B p = pathToIso (cong B p) + +-- Redefining substEquiv in terms of substIso gives an explicit inverse +substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y +substEquiv' B p = isoToEquiv (substIso B p) + +isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B} + → transport p ≡ transport q → p ≡ q +isInjectiveTransport {p = p} {q} α i = + hcomp + (λ j → λ + { (i = i0) → retEq univalence p j + ; (i = i1) → retEq univalence q j + }) + (invEq univalence ((λ a → α i a) , t i)) + where + t : PathP (λ i → isEquiv (λ a → α i a)) (pathToEquiv p .snd) (pathToEquiv q .snd) + t = isProp→PathP (λ i → isPropIsEquiv (λ a → α i a)) _ _ + +transportUaInv : ∀ {ℓ} {A B : Type ℓ} (e : A ≃ B) → transport (ua (invEquiv e)) ≡ transport (sym (ua e)) +transportUaInv e = cong transport (uaInvEquiv e) +-- notice that transport (ua e) would reduce, thus an alternative definition using EquivJ can give +-- refl for the case of idEquiv: +-- transportUaInv e = EquivJ (λ _ e → transport (ua (invEquiv e)) ≡ transport (sym (ua e))) refl e + +isSet-subst : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} + → (isSet-A : isSet A) + → ∀ {a : A} + → (p : a ≡ a) → (x : B a) → subst B p x ≡ x +isSet-subst {B = B} isSet-A p x = subst (λ p′ → subst B p′ x ≡ x) (isSet-A _ _ refl p) (substRefl {B = B} x) + +-- substituting along a composite path is equivalent to substituting twice +substComposite : ∀ {ℓ ℓ'} {A : Type ℓ} → (B : A → Type ℓ') + → {x y z : A} (p : x ≡ y) (q : y ≡ z) (u : B x) + → subst B (p ∙ q) u ≡ subst B q (subst B p u) +substComposite B p q Bx i = + transport (cong B (compPath-filler' p q (~ i))) (transport-fillerExt (cong B p) i Bx) + +-- transporting along a composite path is equivalent to transporting twice +transportComposite : ∀ {ℓ} {A B C : Type ℓ} (p : A ≡ B) (q : B ≡ C) (x : A) + → transport (p ∙ q) x ≡ transport q (transport p x) +transportComposite = substComposite (λ D → D) + +-- substitution commutes with morphisms in slices +substCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} + → (B : A → Type ℓ') (C : A → Type ℓ'') + → (F : ∀ a → B a → C a) + → {x y : A} (p : x ≡ y) (u : B x) + → subst C p (F x u) ≡ F y (subst B p u) +substCommSlice B C F p Bx a = + transport-fillerExt⁻ (cong C p) a (F _ (transport-fillerExt (cong B p) a Bx)) + +constSubstCommSlice : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} + → (B : A → Type ℓ') + → (C : Type ℓ'') + → (F : ∀ a → B a → C) + → {x y : A} (p : x ≡ y) (u : B x) + → (F x u) ≡ F y (subst B p u) +constSubstCommSlice B C F p Bx = (sym (transportRefl (F _ Bx)) ∙ substCommSlice B (λ _ → C) F p Bx) + +-- transporting over (λ i → B (p i) → C (p i)) divides the transport into +-- transports over (λ i → C (p i)) and (λ i → B (p (~ i))) +funTypeTransp : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} (B : A → Type ℓ') (C : A → Type ℓ'') {x y : A} (p : x ≡ y) (f : B x → C x) + → PathP (λ i → B (p i) → C (p i)) f (subst C p ∘ f ∘ subst B (sym p)) +funTypeTransp B C {x = x} p f i b = + transp (λ j → C (p (j ∧ i))) (~ i) (f (transp (λ j → B (p (i ∧ ~ j))) (~ i) b)) + +-- transports between loop spaces preserve path composition +overPathFunct : ∀ {ℓ} {A : Type ℓ} {x y : A} (p q : x ≡ x) (P : x ≡ y) + → transport (λ i → P i ≡ P i) (p ∙ q) + ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q +overPathFunct p q = + J (λ y P → transport (λ i → P i ≡ P i) (p ∙ q) ≡ transport (λ i → P i ≡ P i) p ∙ transport (λ i → P i ≡ P i) q) + (transportRefl (p ∙ q) ∙ cong₂ _∙_ (sym (transportRefl p)) (sym (transportRefl q))) + +-- substition over families of paths +-- theorem 2.11.3 in The Book +substInPaths : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {a a' : A} + → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a) + → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p +substInPaths {a = a} f g p q = + J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p')) + p=refl p + where + p=refl : subst (λ y → f y ≡ g y) refl q + ≡ refl ∙ q ∙ refl + p=refl = subst (λ y → f y ≡ g y) refl q + ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q + ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎ + +flipTransport : ∀ {ℓ} {A : I → Type ℓ} {x : A i0} {y : A i1} + → x ≡ transport⁻ (λ i → A i) y + → transport (λ i → A i) x ≡ y +flipTransport {A = A} {y = y} p = + cong (transport (λ i → A i)) p ∙ transportTransport⁻ (λ i → A i) y + +-- special cases of substInPaths from lemma 2.11.2 in The Book +module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where + substInPathsL : (q : a ≡ x1) → subst (λ x → a ≡ x) p q ≡ q ∙ p + substInPathsL q = subst (λ x → a ≡ x) p q + ≡⟨ substInPaths (λ _ → a) (λ x → x) p q ⟩ + sym (cong (λ _ → a) p) ∙ q ∙ cong (λ x → x) p + ≡⟨ assoc (λ _ → a) q p ⟩ + (refl ∙ q) ∙ p + ≡⟨ cong (_∙ p) (sym (lUnit q)) ⟩ q ∙ p ∎ + + substInPathsR : (q : x1 ≡ a) → subst (λ x → x ≡ a) p q ≡ sym p ∙ q + substInPathsR q = subst (λ x → x ≡ a) p q + ≡⟨ substInPaths (λ x → x) (λ _ → a) p q ⟩ + sym (cong (λ x → x) p) ∙ q ∙ cong (λ _ → a) p + ≡⟨ assoc (sym p) q refl ⟩ + (sym p ∙ q) ∙ refl + ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ \ No newline at end of file diff --git a/Cubical.Foundations.Univalence.Dependent.html b/Cubical.Foundations.Univalence.Dependent.html index 9456c3c814..c4d487c64a 100644 --- a/Cubical.Foundations.Univalence.Dependent.html +++ b/Cubical.Foundations.Univalence.Dependent.html @@ -41,7 +41,7 @@ -- A quick proof provided by @ecavallo. -- Unfortunately it gives a larger term overall. _ : PathP (λ i → ua e i → Type ℓ') P Q - _ = ua→ (λ a → ua (Γ a)) + _ = ua→ (λ a → ua (Γ a)) uaOver : PathP (λ i → ua e i → Type ℓ') P Q uaOver i x = Glue Base {φ} equiv-boundary where diff --git a/Cubical.Foundations.Univalence.Universe.html b/Cubical.Foundations.Univalence.Universe.html index c05e8baf44..56374f68f7 100644 --- a/Cubical.Foundations.Univalence.Universe.html +++ b/Cubical.Foundations.Univalence.Universe.html @@ -45,66 +45,66 @@ reg {A} i z = transp (λ _ → A) i z nu : ∀ x y → x ≡ y → El x ≃ El y - nu x y p = pathToEquiv (cong El p) + nu x y p = pathToEquiv (cong El p) cong-un-te : ∀ x y (p : El x ≡ El y) - → cong El (un x y (pathToEquiv p)) ≡ p + → cong El (un x y (pathToEquiv p)) ≡ p cong-un-te x y p - = comp (pathToEquiv p) ∙ uaTransportη p - - nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e - nu-un x y e - = equivEq {e = nu x y (un x y e)} {f = e} λ i z - → (cong (λ p → transport p z) (comp e) ∙ uaβ e z) i - - El-un-equiv : ∀ x i → El (un x x (idEquiv _) i) ≃ El x - El-un-equiv x i = λ where - .fst → transp (λ j → p j) (i ∨ ~ i) - .snd → transp (λ j → isEquiv (transp (λ k → p (j ∧ k)) (~ j ∨ i ∨ ~ i))) - (i ∨ ~ i) (idIsEquiv T) - where - T = El (un x x (idEquiv _) i) - p : T ≡ El x - p j = (comp (idEquiv _) ∙ uaIdEquiv {A = El x}) j i - - un-refl : ∀ x → un x x (idEquiv (El x)) ≡ refl - un-refl x i j - = hcomp (λ k → λ where - (i = i0) → un x x (idEquiv (El x)) j - (i = i1) → un x x (idEquiv (El x)) (j ∨ k) - (j = i0) → un x x (idEquiv (El x)) (~ i ∨ k) - (j = i1) → x) - (un (un x x (idEquiv (El x)) (~ i)) x (El-un-equiv x (~ i)) j) - - nu-refl : ∀ x → nu x x refl ≡ idEquiv (El x) - nu-refl x = equivEq {e = nu x x refl} {f = idEquiv (El x)} reg - - un-nu : ∀ x y (p : x ≡ y) → un x y (nu x y p) ≡ p - un-nu x y p - = J (λ z q → un x z (nu x z q) ≡ q) (cong (un x x) (nu-refl x) ∙ un-refl x) p - -open UU-Lemmas -open Iso - -equivIso : ∀ s t → Iso (s ≡ t) (El s ≃ El t) -equivIso s t .fun = nu s t -equivIso s t .inv = un s t -equivIso s t .rightInv = nu-un s t -equivIso s t .leftInv = un-nu s t - -pathIso : ∀ s t → Iso (s ≡ t) (El s ≡ El t) -pathIso s t .fun = cong El -pathIso s t .inv = un s t ∘ pathToEquiv -pathIso s t .rightInv = cong-un-te s t -pathIso s t .leftInv = un-nu s t - -minivalence : ∀{s t} → (s ≡ t) ≃ (El s ≃ El t) -minivalence {s} {t} = isoToEquiv (equivIso s t) - -path-reflection : ∀{s t} → (s ≡ t) ≃ (El s ≡ El t) -path-reflection {s} {t} = isoToEquiv (pathIso s t) - -isEmbeddingEl : isEmbedding El -isEmbeddingEl s t = snd path-reflection + = comp (pathToEquiv p) ∙ uaη p + + nu-un : ∀ x y (e : El x ≃ El y) → nu x y (un x y e) ≡ e + nu-un x y e + = equivEq {e = nu x y (un x y e)} {f = e} λ i z + → (cong (λ p → transport p z) (comp e) ∙ uaβ e z) i + + El-un-equiv : ∀ x i → El (un x x (idEquiv _) i) ≃ El x + El-un-equiv x i = λ where + .fst → transp (λ j → p j) (i ∨ ~ i) + .snd → transp (λ j → isEquiv (transp (λ k → p (j ∧ k)) (~ j ∨ i ∨ ~ i))) + (i ∨ ~ i) (idIsEquiv T) + where + T = El (un x x (idEquiv _) i) + p : T ≡ El x + p j = (comp (idEquiv _) ∙ uaIdEquiv {A = El x}) j i + + un-refl : ∀ x → un x x (idEquiv (El x)) ≡ refl + un-refl x i j + = hcomp (λ k → λ where + (i = i0) → un x x (idEquiv (El x)) j + (i = i1) → un x x (idEquiv (El x)) (j ∨ k) + (j = i0) → un x x (idEquiv (El x)) (~ i ∨ k) + (j = i1) → x) + (un (un x x (idEquiv (El x)) (~ i)) x (El-un-equiv x (~ i)) j) + + nu-refl : ∀ x → nu x x refl ≡ idEquiv (El x) + nu-refl x = equivEq {e = nu x x refl} {f = idEquiv (El x)} reg + + un-nu : ∀ x y (p : x ≡ y) → un x y (nu x y p) ≡ p + un-nu x y p + = J (λ z q → un x z (nu x z q) ≡ q) (cong (un x x) (nu-refl x) ∙ un-refl x) p + +open UU-Lemmas +open Iso + +equivIso : ∀ s t → Iso (s ≡ t) (El s ≃ El t) +equivIso s t .fun = nu s t +equivIso s t .inv = un s t +equivIso s t .rightInv = nu-un s t +equivIso s t .leftInv = un-nu s t + +pathIso : ∀ s t → Iso (s ≡ t) (El s ≡ El t) +pathIso s t .fun = cong El +pathIso s t .inv = un s t ∘ pathToEquiv +pathIso s t .rightInv = cong-un-te s t +pathIso s t .leftInv = un-nu s t + +minivalence : ∀{s t} → (s ≡ t) ≃ (El s ≃ El t) +minivalence {s} {t} = isoToEquiv (equivIso s t) + +path-reflection : ∀{s t} → (s ≡ t) ≃ (El s ≡ El t) +path-reflection {s} {t} = isoToEquiv (pathIso s t) + +isEmbeddingEl : isEmbedding El +isEmbeddingEl s t = snd path-reflection \ No newline at end of file diff --git a/Cubical.Foundations.Univalence.html b/Cubical.Foundations.Univalence.html index cf875b4e83..50e0aa3961 100644 --- a/Cubical.Foundations.Univalence.html +++ b/Cubical.Foundations.Univalence.html @@ -171,154 +171,175 @@ → (r : P B (idEquiv B)) → (e : A ≃ B) → P A e EquivJ P r e = subst (λ x → P (x .fst) (x .snd)) (contrSinglEquiv e) r --- Assuming that we have an inverse to ua we can easily prove univalence -module Univalence (au : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B) - (aurefl : ∀ {ℓ} {A : Type ℓ} → au refl ≡ idEquiv A) where - - ua-au : {A B : Type ℓ} (p : A ≡ B) → ua (au p) ≡ p - ua-au {B = B} = J (λ _ p → ua (au p) ≡ p) - (cong ua aurefl ∙ uaIdEquiv) - - au-ua : {A B : Type ℓ} (e : A ≃ B) → au (ua e) ≡ e - au-ua {B = B} = EquivJ (λ _ f → au (ua f) ≡ f) - (subst (λ r → au r ≡ idEquiv _) (sym uaIdEquiv) aurefl) - - isoThm : ∀ {ℓ} {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B) - isoThm .Iso.fun = au - isoThm .Iso.inv = ua - isoThm .Iso.rightInv = au-ua - isoThm .Iso.leftInv = ua-au - - thm : ∀ {ℓ} {A B : Type ℓ} → isEquiv au - thm {A = A} {B = B} = isoToIsEquiv {B = A ≃ B} isoThm - -isEquivTransport : {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p) -isEquivTransport p = - transport (λ i → isEquiv (transp (λ j → p (i ∧ j)) (~ i))) (idIsEquiv _) - -pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B -pathToEquiv p .fst = transport p -pathToEquiv p .snd = isEquivTransport p - -pathToEquivRefl : {A : Type ℓ} → pathToEquiv refl ≡ idEquiv A -pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x) - -pathToEquiv-ua : {A B : Type ℓ} (e : A ≃ B) → pathToEquiv (ua e) ≡ e -pathToEquiv-ua = Univalence.au-ua pathToEquiv pathToEquivRefl - -ua-pathToEquiv : {A B : Type ℓ} (p : A ≡ B) → ua (pathToEquiv p) ≡ p -ua-pathToEquiv = Univalence.ua-au pathToEquiv pathToEquivRefl - --- Univalence -univalenceIso : {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B) -univalenceIso = Univalence.isoThm pathToEquiv pathToEquivRefl - -univalence : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) -univalence = ( pathToEquiv , Univalence.thm pathToEquiv pathToEquivRefl ) - --- The original map from UniMath/Foundations -eqweqmap : {A B : Type ℓ} → A ≡ B → A ≃ B -eqweqmap {A = A} e = J (λ X _ → A ≃ X) (idEquiv A) e - -eqweqmapid : {A : Type ℓ} → eqweqmap refl ≡ idEquiv A -eqweqmapid {A = A} = JRefl (λ X _ → A ≃ X) (idEquiv A) - -univalenceStatement : {A B : Type ℓ} → isEquiv (eqweqmap {ℓ} {A} {B}) -univalenceStatement = Univalence.thm eqweqmap eqweqmapid - -univalenceUAH : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) -univalenceUAH = ( _ , univalenceStatement ) - -univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift (A ≃ B) -univalencePath = ua (compEquiv univalence LiftEquiv) - --- The computation rule for ua. Because of "ghcomp" it is now very --- simple compared to cubicaltt: --- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202 -uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x -uaβ e x = transportRefl (equivFun e x) - -uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P -uaη = J (λ _ q → ua (pathToEquiv q) ≡ q) (cong ua pathToEquivRefl ∙ uaIdEquiv) - --- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua. -ua→ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'} - {f₀ : A₀ → B i0} {f₁ : A₁ → B i1} - → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a))) - → PathP (λ i → ua e i → B i) f₀ f₁ -ua→ {e = e} {f₀ = f₀} {f₁} h i a = - hcomp - (λ j → λ - { (i = i0) → f₀ a - ; (i = i1) → f₁ (lem a j) - }) - (h (transp (λ j → ua e (~ j ∧ i)) (~ i) a) i) - where - lem : ∀ a₁ → e .fst (transport (sym (ua e)) a₁) ≡ a₁ - lem a₁ = secEq e _ ∙ transportRefl _ - -ua→⁻ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'} - {f₀ : A₀ → B i0} {f₁ : A₁ → B i1} - → PathP (λ i → ua e i → B i) f₀ f₁ - → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a))) -ua→⁻ {e = e} {f₀ = f₀} {f₁} p a i = - hcomp - (λ k → λ - { (i = i0) → f₀ a - ; (i = i1) → f₁ (uaβ e a k) - }) - (p i (transp (λ j → ua e (j ∧ i)) (~ i) a)) - -ua→2 : ∀ {ℓ ℓ' ℓ''} {A₀ A₁ : Type ℓ} {e₁ : A₀ ≃ A₁} - {B₀ B₁ : Type ℓ'} {e₂ : B₀ ≃ B₁} - {C : (i : I) → Type ℓ''} - {f₀ : A₀ → B₀ → C i0} {f₁ : A₁ → B₁ → C i1} - → (∀ a b → PathP C (f₀ a b) (f₁ (e₁ .fst a) (e₂ .fst b))) - → PathP (λ i → ua e₁ i → ua e₂ i → C i) f₀ f₁ -ua→2 h = ua→ (ua→ ∘ h) - --- Useful lemma for unfolding a transported function over ua --- If we would have regularity this would be refl -transportUAop₁ : ∀ {A B : Type ℓ} → (e : A ≃ B) (f : A → A) (x : B) - → transport (λ i → ua e i → ua e i) f x ≡ equivFun e (f (invEq e x)) -transportUAop₁ e f x i = transportRefl (equivFun e (f (invEq e (transportRefl x i)))) i - --- Binary version -transportUAop₂ : ∀ {ℓ} {A B : Type ℓ} → (e : A ≃ B) (f : A → A → A) (x y : B) - → transport (λ i → ua e i → ua e i → ua e i) f x y ≡ - equivFun e (f (invEq e x) (invEq e y)) -transportUAop₂ e f x y i = - transportRefl (equivFun e (f (invEq e (transportRefl x i)) - (invEq e (transportRefl y i)))) i - --- Alternative version of EquivJ that only requires a predicate on functions -elimEquivFun : {A B : Type ℓ} (P : (A : Type ℓ) → (A → B) → Type ℓ') - → (r : P B (idfun B)) → (e : A ≃ B) → P A (e .fst) -elimEquivFun P r e = subst (λ x → P (x .fst) (x .snd .fst)) (contrSinglEquiv e) r - --- Isomorphism induction -elimIso : {B : Type ℓ} → (Q : {A : Type ℓ} → (A → B) → (B → A) → Type ℓ') → - (h : Q (idfun B) (idfun B)) → {A : Type ℓ} → - (f : A → B) → (g : B → A) → section f g → retract f g → Q f g -elimIso {ℓ} {ℓ'} {B} Q h {A} f g sfg rfg = rem1 f g sfg rfg - where - P : (A : Type ℓ) → (f : A → B) → Type (ℓ-max ℓ' ℓ) - P A f = (g : B → A) → section f g → retract f g → Q f g - - rem : P B (idfun B) - rem g sfg rfg = subst (Q (idfun B)) (λ i b → (sfg b) (~ i)) h - - rem1 : {A : Type ℓ} → (f : A → B) → P A f - rem1 f g sfg rfg = elimEquivFun P rem (f , isoToIsEquiv (iso f g sfg rfg)) g sfg rfg - - -uaInvEquiv : ∀ {A B : Type ℓ} → (e : A ≃ B) → ua (invEquiv e) ≡ sym (ua e) -uaInvEquiv {B = B} = EquivJ (λ _ e → ua (invEquiv e) ≡ sym (ua e)) - (cong ua (invEquivIdEquiv B)) - -uaCompEquiv : ∀ {A B C : Type ℓ} → (e : A ≃ B) (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f -uaCompEquiv {B = B} {C} = EquivJ (λ _ e → (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f) - (λ f → cong ua (compEquivIdEquiv f) - ∙ sym (cong (λ x → x ∙ ua f) uaIdEquiv - ∙ sym (lUnit (ua f)))) +-- Transport along a path is an equivalence. +-- The proof is a special case of isEquivTransp where the line of types is +-- given by p, and the extend φ -- where the transport is constant -- is i0. +isEquivTransport : {A B : Type ℓ} (p : A ≡ B) → isEquiv (transport p) +isEquivTransport p = isEquivTransp A φ where + A : I → Type _ + A i = p i + + φ : I + φ = i0 + +pathToEquiv : {A B : Type ℓ} → A ≡ B → A ≃ B +pathToEquiv p .fst = transport p +pathToEquiv p .snd = isEquivTransport p + +pathToEquivRefl : {A : Type ℓ} → pathToEquiv refl ≡ idEquiv A +pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x) + +-- The computation rule for ua. Because of "ghcomp" it is now very +-- simple compared to cubicaltt: +-- https://github.com/mortberg/cubicaltt/blob/master/examples/univalence.ctt#L202 +uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x +uaβ e x = transportRefl (equivFun e x) + +uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P +uaη {A = A} {B = B} P i j = Glue B {φ = φ} sides where + -- Adapted from a proof by @dolio, cf. commit e42a6fa1 + φ = i ∨ j ∨ ~ j + + sides : Partial φ (Σ[ T ∈ Type _ ] T ≃ B) + sides (i = i1) = P j , transpEquiv (λ k → P k) j + sides (j = i0) = A , pathToEquiv P + sides (j = i1) = B , idEquiv B + +pathToEquiv-ua : {A B : Type ℓ} (e : A ≃ B) → pathToEquiv (ua e) ≡ e +pathToEquiv-ua e = equivEq (funExt (uaβ e)) + +ua-pathToEquiv : {A B : Type ℓ} (p : A ≡ B) → ua (pathToEquiv p) ≡ p +ua-pathToEquiv = uaη + +-- Univalence +univalenceIso : {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B) +univalenceIso .Iso.fun = pathToEquiv +univalenceIso .Iso.inv = ua +univalenceIso .Iso.rightInv = pathToEquiv-ua +univalenceIso .Iso.leftInv = ua-pathToEquiv + +isEquivPathToEquiv : {A B : Type ℓ} → isEquiv (pathToEquiv {A = A} {B = B}) +isEquivPathToEquiv = isoToIsEquiv univalenceIso + +univalence : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) +univalence .fst = pathToEquiv +univalence .snd = isEquivPathToEquiv + +-- Assuming that we have an inverse to ua we can easily prove univalence +module Univalence (au : ∀ {ℓ} {A B : Type ℓ} → A ≡ B → A ≃ B) + (aurefl : ∀ {ℓ} {A : Type ℓ} → au refl ≡ idEquiv A) where + + ua-au : {A B : Type ℓ} (p : A ≡ B) → ua (au p) ≡ p + ua-au {B = B} = J (λ _ p → ua (au p) ≡ p) + (cong ua aurefl ∙ uaIdEquiv) + + au-ua : {A B : Type ℓ} (e : A ≃ B) → au (ua e) ≡ e + au-ua {B = B} = EquivJ (λ _ f → au (ua f) ≡ f) + (subst (λ r → au r ≡ idEquiv _) (sym uaIdEquiv) aurefl) + + isoThm : ∀ {ℓ} {A B : Type ℓ} → Iso (A ≡ B) (A ≃ B) + isoThm .Iso.fun = au + isoThm .Iso.inv = ua + isoThm .Iso.rightInv = au-ua + isoThm .Iso.leftInv = ua-au + + thm : ∀ {ℓ} {A B : Type ℓ} → isEquiv au + thm {A = A} {B = B} = isoToIsEquiv {B = A ≃ B} isoThm + +-- The original map from UniMath/Foundations +eqweqmap : {A B : Type ℓ} → A ≡ B → A ≃ B +eqweqmap {A = A} e = J (λ X _ → A ≃ X) (idEquiv A) e + +eqweqmapid : {A : Type ℓ} → eqweqmap refl ≡ idEquiv A +eqweqmapid {A = A} = JRefl (λ X _ → A ≃ X) (idEquiv A) + +univalenceStatement : {A B : Type ℓ} → isEquiv (eqweqmap {ℓ} {A} {B}) +univalenceStatement = Univalence.thm eqweqmap eqweqmapid + +univalenceUAH : {A B : Type ℓ} → (A ≡ B) ≃ (A ≃ B) +univalenceUAH = ( _ , univalenceStatement ) + +univalencePath : {A B : Type ℓ} → (A ≡ B) ≡ Lift (A ≃ B) +univalencePath = ua (compEquiv univalence LiftEquiv) + +-- Lemmas for constructing and destructing dependent paths in a function type where the domain is ua. +ua→ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'} + {f₀ : A₀ → B i0} {f₁ : A₁ → B i1} + → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a))) + → PathP (λ i → ua e i → B i) f₀ f₁ +ua→ {e = e} {f₀ = f₀} {f₁} h i a = + hcomp + (λ j → λ + { (i = i0) → f₀ a + ; (i = i1) → f₁ (lem a j) + }) + (h (transp (λ j → ua e (~ j ∧ i)) (~ i) a) i) + where + lem : ∀ a₁ → e .fst (transport (sym (ua e)) a₁) ≡ a₁ + lem a₁ = secEq e _ ∙ transportRefl _ + +ua→⁻ : ∀ {ℓ ℓ'} {A₀ A₁ : Type ℓ} {e : A₀ ≃ A₁} {B : (i : I) → Type ℓ'} + {f₀ : A₀ → B i0} {f₁ : A₁ → B i1} + → PathP (λ i → ua e i → B i) f₀ f₁ + → ((a : A₀) → PathP B (f₀ a) (f₁ (e .fst a))) +ua→⁻ {e = e} {f₀ = f₀} {f₁} p a i = + hcomp + (λ k → λ + { (i = i0) → f₀ a + ; (i = i1) → f₁ (uaβ e a k) + }) + (p i (transp (λ j → ua e (j ∧ i)) (~ i) a)) + +ua→2 : ∀ {ℓ ℓ' ℓ''} {A₀ A₁ : Type ℓ} {e₁ : A₀ ≃ A₁} + {B₀ B₁ : Type ℓ'} {e₂ : B₀ ≃ B₁} + {C : (i : I) → Type ℓ''} + {f₀ : A₀ → B₀ → C i0} {f₁ : A₁ → B₁ → C i1} + → (∀ a b → PathP C (f₀ a b) (f₁ (e₁ .fst a) (e₂ .fst b))) + → PathP (λ i → ua e₁ i → ua e₂ i → C i) f₀ f₁ +ua→2 h = ua→ (ua→ ∘ h) + +-- Useful lemma for unfolding a transported function over ua +-- If we would have regularity this would be refl +transportUAop₁ : ∀ {A B : Type ℓ} → (e : A ≃ B) (f : A → A) (x : B) + → transport (λ i → ua e i → ua e i) f x ≡ equivFun e (f (invEq e x)) +transportUAop₁ e f x i = transportRefl (equivFun e (f (invEq e (transportRefl x i)))) i + +-- Binary version +transportUAop₂ : ∀ {ℓ} {A B : Type ℓ} → (e : A ≃ B) (f : A → A → A) (x y : B) + → transport (λ i → ua e i → ua e i → ua e i) f x y ≡ + equivFun e (f (invEq e x) (invEq e y)) +transportUAop₂ e f x y i = + transportRefl (equivFun e (f (invEq e (transportRefl x i)) + (invEq e (transportRefl y i)))) i + +-- Alternative version of EquivJ that only requires a predicate on functions +elimEquivFun : {A B : Type ℓ} (P : (A : Type ℓ) → (A → B) → Type ℓ') + → (r : P B (idfun B)) → (e : A ≃ B) → P A (e .fst) +elimEquivFun P r e = subst (λ x → P (x .fst) (x .snd .fst)) (contrSinglEquiv e) r + +-- Isomorphism induction +elimIso : {B : Type ℓ} → (Q : {A : Type ℓ} → (A → B) → (B → A) → Type ℓ') → + (h : Q (idfun B) (idfun B)) → {A : Type ℓ} → + (f : A → B) → (g : B → A) → section f g → retract f g → Q f g +elimIso {ℓ} {ℓ'} {B} Q h {A} f g sfg rfg = rem1 f g sfg rfg + where + P : (A : Type ℓ) → (f : A → B) → Type (ℓ-max ℓ' ℓ) + P A f = (g : B → A) → section f g → retract f g → Q f g + + rem : P B (idfun B) + rem g sfg rfg = subst (Q (idfun B)) (λ i b → (sfg b) (~ i)) h + + rem1 : {A : Type ℓ} → (f : A → B) → P A f + rem1 f g sfg rfg = elimEquivFun P rem (f , isoToIsEquiv (iso f g sfg rfg)) g sfg rfg + + +uaInvEquiv : ∀ {A B : Type ℓ} → (e : A ≃ B) → ua (invEquiv e) ≡ sym (ua e) +uaInvEquiv {B = B} = EquivJ (λ _ e → ua (invEquiv e) ≡ sym (ua e)) + (cong ua (invEquivIdEquiv B)) + +uaCompEquiv : ∀ {A B C : Type ℓ} → (e : A ≃ B) (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f +uaCompEquiv {B = B} {C} = EquivJ (λ _ e → (f : B ≃ C) → ua (compEquiv e f) ≡ ua e ∙ ua f) + (λ f → cong ua (compEquivIdEquiv f) + ∙ sym (cong (λ x → x ∙ ua f) uaIdEquiv + ∙ sym (lUnit (ua f)))) \ No newline at end of file diff --git a/Cubical.Functions.Bundle.html b/Cubical.Functions.Bundle.html index 5a146dbdc2..dc1d8aa918 100644 --- a/Cubical.Functions.Bundle.html +++ b/Cubical.Functions.Bundle.html @@ -44,7 +44,7 @@ -} bundleEquiv : (B → TypeEqvTo ℓ' F) ≃ (Σ[ E ∈ Type ℓ' ] Σ[ p ∈ (E → B) ] ∀ x → ∥ fiber p x ≃ F ∥₁) - bundleEquiv = compEquiv (compEquiv Σ-Π-≃ (pathToEquiv p)) Σ-assoc-≃ + bundleEquiv = compEquiv (compEquiv Σ-Π-≃ (pathToEquiv p)) Σ-assoc-≃ where e = fibrationEquiv B ℓ p : (Σ[ p⁻¹ ∈ (B → Type ℓ') ] ∀ x → ∥ p⁻¹ x ≃ F ∥₁) ≡ (Σ[ p ∈ (Σ[ E ∈ Type ℓ' ] (E → B)) ] ∀ x → ∥ fiber (snd p) x ≃ F ∥₁ ) diff --git a/Cubical.Functions.Embedding.html b/Cubical.Functions.Embedding.html index 30cbb99736..0b1480d869 100644 --- a/Cubical.Functions.Embedding.html +++ b/Cubical.Functions.Embedding.html @@ -13,7 +13,7 @@ open import Cubical.Foundations.Powerset open import Cubical.Foundations.Prelude open import Cubical.Foundations.Transport -open import Cubical.Foundations.Univalence using (ua; univalence; pathToEquiv) +open import Cubical.Foundations.Univalence using (ua; univalence; pathToEquiv) open import Cubical.Functions.Fibration open import Cubical.Data.Sigma @@ -315,10 +315,10 @@ → isEmbedding F universeEmbedding F liftingEquiv = hasPropFibersOfImage→isEmbedding propFibersF where lemma : ∀ A B → (F A ≡ F B) ≃ (B ≡ A) - lemma A B = (F A ≡ F B) ≃⟨ univalence ⟩ + lemma A B = (F A ≡ F B) ≃⟨ univalence ⟩ (F A ≃ F B) ≃⟨ equivComp (liftingEquiv A) (liftingEquiv B) ⟩ (A ≃ B) ≃⟨ invEquivEquiv ⟩ - (B ≃ A) ≃⟨ invEquiv univalence ⟩ + (B ≃ A) ≃⟨ invEquiv univalence ⟩ (B ≡ A) ■ fiberSingl : ∀ X → fiber F (F X) ≃ singl X fiberSingl X = Σ-cong-equiv-snd (λ _ → lemma _ _) @@ -343,7 +343,7 @@ Fibration′IP : f≃g′ ≃ (f ≡ g) Fibration′IP = f≃g′ - ≃⟨ equivΠCod (λ _ → invEquiv univalence) ⟩ + ≃⟨ equivΠCod (λ _ → invEquiv univalence) ⟩ (∀ b → fiber (f .snd) b ≡ fiber (g .snd) b) ≃⟨ funExtEquiv ⟩ fiber (f .snd) ≡ fiber (g .snd) @@ -365,15 +365,15 @@ λ _ → isEquiv→hasPropFibers (snd (invEquiv (preCompEquiv LiftEquiv))) _) where fiberChar : fiber liftFibration (A , f) - ≃ (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f)) + ≃ (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f)) fiberChar = fiber liftFibration (A , f) ≃⟨ Σ-cong-equiv-snd (λ _ → invEquiv ΣPath≃PathΣ) ⟩ (Σ[ (E , g) ∈ Fibration B ℓ' ] Σ[ eq ∈ (L E ≡ A) ] PathP (λ i → eq i → B) (g ∘ lower) f) ≃⟨ boringSwap ⟩ (Σ[ (E , eq) ∈ fiber L A ] Σ[ g ∈ (E → B) ] PathP (λ i → eq i → B) (g ∘ lower) f) - ≃⟨ Σ-cong-equiv-snd (λ _ → Σ-cong-equiv-snd λ _ → pathToEquiv (PathP≡Path⁻ _ _ _)) ⟩ - (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f)) + ≃⟨ Σ-cong-equiv-snd (λ _ → Σ-cong-equiv-snd λ _ → pathToEquiv (PathP≡Path⁻ _ _ _)) ⟩ + (Σ[ (E , eq) ∈ fiber L A ] fiber (_∘ lower) (transport⁻ (λ i → eq i → B) f)) ■ where unquoteDecl boringSwap = declStrictEquiv boringSwap diff --git a/Cubical.Functions.Fibration.html b/Cubical.Functions.Fibration.html index e4f162d9ec..45af7e9f33 100644 --- a/Cubical.Functions.Fibration.html +++ b/Cubical.Functions.Fibration.html @@ -41,7 +41,7 @@ ((x , refl ) , subst p⁻¹ q y) ((x' , sym q) , y ) r = ΣPathP (isContrSingl x .snd (x' , sym q) - , toPathP (transport⁻Transport (λ i → p⁻¹ (q i)) y)) + , toPathP (transport⁻Transport (λ i → p⁻¹ (q i)) y)) -- HoTT Lemma 4.8.1 fiberEquiv : fiber p x ≃ p⁻¹ x diff --git a/Cubical.Functions.Involution.html b/Cubical.Functions.Involution.html index ca93bf9fcb..4a8cc37236 100644 --- a/Cubical.Functions.Involution.html +++ b/Cubical.Functions.Involution.html @@ -35,7 +35,7 @@ involPathComp : involPath ∙ involPath ≡ refl involPathComp - = sym (uaCompEquiv involEquiv involEquiv) ∙∙ cong ua involEquivComp ∙∙ uaIdEquiv + = sym (uaCompEquiv involEquiv involEquiv) ∙∙ cong ua involEquivComp ∙∙ uaIdEquiv involPath² : Square involPath refl refl involPath involPath² diff --git a/Cubical.HITs.Bouquet.FundamentalGroupProof.html b/Cubical.HITs.Bouquet.FundamentalGroupProof.html index b72ba9aaf4..1506ed62c1 100644 --- a/Cubical.HITs.Bouquet.FundamentalGroupProof.html +++ b/Cubical.HITs.Bouquet.FundamentalGroupProof.html @@ -137,7 +137,7 @@ subst code (sym (loop a)) g ≡⟨ cong (λ x → transport x g) (sym (invPathsInUNaturality (η a))) ⟩ transport (pathsInU (inv (η a))) g - ≡⟨ uaβ (equivs (inv (η a))) g ⟩ + ≡⟨ uaβ (equivs (inv (η a))) g ⟩ action (inv (η a)) g ∎ calculations : ∀ (a : A) → ∀ g → looping (g · (inv (η a))) ∙ loop a ≡ looping g calculations a g = @@ -228,7 +228,7 @@ winding (looping g) ≡⟨ cong (λ x → transport x ε) hyp ⟩ transport (ua (equivs g)) ε - ≡⟨ uaβ (equivs g) ε ⟩ + ≡⟨ uaβ (equivs g) ε ⟩ ε · g ≡⟨ sym (idl g) ⟩ g ∎ diff --git a/Cubical.HITs.FreeGroupoid.GroupoidActions.html b/Cubical.HITs.FreeGroupoid.GroupoidActions.html index 1b450ba971..dcf5e9315d 100644 --- a/Cubical.HITs.FreeGroupoid.GroupoidActions.html +++ b/Cubical.HITs.FreeGroupoid.GroupoidActions.html @@ -131,7 +131,7 @@ pathsInU (g1 · g2) ≡⟨ cong ua (multEquivsNaturality g1 g2) ⟩ ua (compEquiv (equivs g1) (equivs g2)) - ≡⟨ uaCompEquiv (equivs g1) (equivs g2) ⟩ + ≡⟨ uaCompEquiv (equivs g1) (equivs g2) ⟩ (pathsInU g1) ∙ (pathsInU g2) ∎ idPathsInUNaturality : pathsInU {A = A} ε ≡ refl @@ -147,6 +147,6 @@ pathsInU (inv g) ≡⟨ cong ua (invEquivsNaturality g) ⟩ ua (invEquiv (equivs g)) - ≡⟨ uaInvEquiv (equivs g) ⟩ + ≡⟨ uaInvEquiv (equivs g) ⟩ sym (pathsInU g) ∎ \ No newline at end of file diff --git a/Cubical.HITs.James.Inductive.Reduced.html b/Cubical.HITs.James.Inductive.Reduced.html index 7514778824..3a754fb520 100644 --- a/Cubical.HITs.James.Inductive.Reduced.html +++ b/Cubical.HITs.James.Inductive.Reduced.html @@ -215,7 +215,7 @@ -- The main equivalence: 𝕁ames∞≃𝕁Red∞ : 𝕁ames∞ ≃ 𝕁Red∞ - 𝕁ames∞≃𝕁Red∞ = compEquiv 𝕁ames∞≃𝕁0∞ (compEquiv (pathToEquiv (λ i → 𝕁Path∞ i)) 𝕁1∞≃𝕁Red∞) + 𝕁ames∞≃𝕁Red∞ = compEquiv 𝕁ames∞≃𝕁0∞ (compEquiv (pathToEquiv (λ i → 𝕁Path∞ i)) 𝕁1∞≃𝕁Red∞) -- Test of canonicity diff --git a/Cubical.HITs.Nullification.Properties.html b/Cubical.HITs.Nullification.Properties.html index c937994b55..ddebb94834 100644 --- a/Cubical.HITs.Nullification.Properties.html +++ b/Cubical.HITs.Nullification.Properties.html @@ -60,7 +60,7 @@ rec nB g (≡hub {x} {y} {α} p i) = fst (secCong (nB α) (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i rec nB g (≡spoke {x} {y} {α} p s i j) = snd (secCong (nB α) (rec nB g x) (rec nB g y)) (λ i s → rec nB g (p s i)) i j s -toPathP⁻ : ∀ {ℓ} (A : I → Type ℓ) {x : A i0} {y : A i1} → x ≡ transport⁻ (λ i → A i) y → PathP A x y +toPathP⁻ : ∀ {ℓ} (A : I → Type ℓ) {x : A i0} {y : A i1} → x ≡ transport⁻ (λ i → A i) y → PathP A x y toPathP⁻ A p i = toPathP {A = λ i → A (~ i)} (sym p) (~ i) toPathP⁻-sq : ∀ {ℓ} {A : Type ℓ} (x : A) → Square (toPathP⁻ (λ _ → A) (λ _ → transport refl x)) refl diff --git a/Cubical.HITs.Pushout.Properties.html b/Cubical.HITs.Pushout.Properties.html index bde9b6e74b..54042217da 100644 --- a/Cubical.HITs.Pushout.Properties.html +++ b/Cubical.HITs.Pushout.Properties.html @@ -123,16 +123,16 @@ spanPath2 i = record { A0 = A0 s2 ; A2 = A2 s2 ; A4 = A4 s2 ; f1 = f1Path i ; f3 = f3Path i } where f1Path : I → A2 s2 → A0 s2 - f1Path i x = ((uaβ e0 (f1 s1 (transport (λ j → path2 (~ j)) x))) + f1Path i x = ((uaβ e0 (f1 s1 (transport (λ j → path2 (~ j)) x))) ∙ (H1 (transport (λ j → path2 (~ j)) x)) ⁻¹ - ∙ (λ j → f1 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j))) - ∙ (λ j → f1 s2 (transportTransport⁻ path2 x j))) i + ∙ (λ j → f1 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j))) + ∙ (λ j → f1 s2 (transportTransport⁻ path2 x j))) i f3Path : I → A2 s2 → A4 s2 - f3Path i x = ((uaβ e4 (f3 s1 (transport (λ j → path2 (~ j)) x))) + f3Path i x = ((uaβ e4 (f3 s1 (transport (λ j → path2 (~ j)) x))) ∙ (H3 (transport (λ j → path2 (~ j)) x)) ⁻¹ - ∙ (λ j → f3 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j))) - ∙ (λ j → f3 s2 (transportTransport⁻ path2 x j))) i + ∙ (λ j → f3 s2 (uaβ e2 (transport (λ j → path2 (~ j)) x) (~ j))) + ∙ (λ j → f3 s2 (transportTransport⁻ path2 x j))) i spanPath : s1 ≡ s2 spanPath = (λ i → spanPath1 i) ∙ (λ i → spanPath2 i) diff --git a/Cubical.HITs.RPn.Base.html b/Cubical.HITs.RPn.Base.html index 43a67a7d9b..0a2d4d89cf 100644 --- a/Cubical.HITs.RPn.Base.html +++ b/Cubical.HITs.RPn.Base.html @@ -277,7 +277,7 @@ ; H3 = λ x → cong snd (H x) } ii : Pushout Σf Σg ≃ join (Total (cov⁻¹ (-1+ n))) Bool - ii = compEquiv (pathToEquiv (spanEquivToPushoutPath nat)) (joinPushout≃join _ _) + ii = compEquiv (pathToEquiv (spanEquivToPushoutPath nat)) (joinPushout≃join _ _) {- (iii) Finally, it's trivial to show that `join (Total (cov⁻¹ (n-1))) Bool` is equivalent to diff --git a/Cubical.HITs.SmashProduct.Base.html b/Cubical.HITs.SmashProduct.Base.html index 7c5b9c0fc0..02ba2f783f 100644 --- a/Cubical.HITs.SmashProduct.Base.html +++ b/Cubical.HITs.SmashProduct.Base.html @@ -123,7 +123,7 @@ is₂ = compIso is₁ (Σ-cong-iso-snd λ f → Σ-cong-iso-snd λ l → Σ-cong-iso-snd - λ r → pathToIso (PathP≡doubleCompPathʳ _ _ _ _ + λ r → pathToIso (PathP≡doubleCompPathʳ _ _ _ _ ∙ cong (l (snd A) ≡_) (sym (compPath≡compPath' (r (snd B)) refl) ∙ sym (rUnit (r (pt B)))))) diff --git a/Cubical.Homotopy.Connected.html b/Cubical.Homotopy.Connected.html index cfccb42fea..8288780f22 100644 --- a/Cubical.Homotopy.Connected.html +++ b/Cubical.Homotopy.Connected.html @@ -591,7 +591,7 @@ k (inr x) = h x k (push a i) = hcomp (λ k → λ { (i = i0) → equiv-proof (elim.isEquivPrecompose f n Q iscon) fun .fst .snd i0 a - ; (i = i1) → transportTransport⁻ (λ j → typ (P (push a j))) (h (g a)) k }) + ; (i = i1) → transportTransport⁻ (λ j → typ (P (push a j))) (h (g a)) k }) (transp (λ j → typ (P (push a (i ∧ j)))) (~ i) (equiv-proof (elim.isEquivPrecompose f n Q iscon) @@ -798,7 +798,7 @@ X' a' = Σ[ x' ∈ (Unit → P (inl a') .fst) ] (λ (b : B) → x' tt) ≡ - (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b))) + (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b))) X≃X' : (a' : A') → X a' ≃ X' a' X≃X' a' = @@ -807,13 +807,13 @@ ≃⟨ invEquiv (Σ-cong-equiv-fst (UnitToType≃ _)) ⟩ (Σ[ x' ∈ (Unit → P (inl a') .fst) ] ∀ (b : B) → PathP (λ i → P (push a' b i) .fst) (x' tt) (k (inr b))) - ≃⟨ Σ-cong-equiv-snd (λ x' → equivΠCod (λ b → pathToEquiv (PathP≡Path⁻ _ _ _))) ⟩ + ≃⟨ Σ-cong-equiv-snd (λ x' → equivΠCod (λ b → pathToEquiv (PathP≡Path⁻ _ _ _))) ⟩ (Σ[ x' ∈ (Unit → P (inl a') .fst) ] - ∀ (b : B) → x' tt ≡ subst⁻ (λ y → P y .fst) (push a' b) (k (inr b))) + ∀ (b : B) → x' tt ≡ subst⁻ (λ y → P y .fst) (push a' b) (k (inr b))) ≃⟨ Σ-cong-equiv-snd (λ x' → funExtEquiv) ⟩ (Σ[ x' ∈ (Unit → P (inl a') .fst) ] (λ (b : B) → x' tt) ≡ - (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b)))) + (λ (b : B) → subst⁻ (λ y → P y .fst) (push a' b) (k (inr b)))) ■ X'level : (a' : A') → isOfHLevel m (X' a') diff --git a/Cubical.Homotopy.EilenbergMacLane.CupProduct.html b/Cubical.Homotopy.EilenbergMacLane.CupProduct.html index c494924a2a..c54767c434 100644 --- a/Cubical.Homotopy.EilenbergMacLane.CupProduct.html +++ b/Cubical.Homotopy.EilenbergMacLane.CupProduct.html @@ -82,7 +82,7 @@ ⌣ₖ-1ₖ : (n : ℕ) (x : EM G' n) → (x ⌣ₖ 1ₖ) ≡ subst (EM G') (+'-comm zero n) x ⌣ₖ-1ₖ n x = cong (EMTensorMult (n +' zero)) (Neutral.⌣ₖ-1ₖ n x) - ∙∙ sym (substCommSlice (EM (G' ⨂ G')) (EM G') + ∙∙ sym (substCommSlice (EM (G' ⨂ G')) (EM G') EMTensorMult (+'-comm zero n) (inducedFun-EM (lIncl⨂ 1ₖ) n x)) ∙∙ cong (subst (EM G') (+'-comm zero n)) @@ -115,7 +115,7 @@ assoc⌣ₖ n m l x y z = EMTensorMultDistrLem _ _ (x ⌣ₖ⊗ y) z ∙ cong (EMTensorMult3ₗ ((n +' m) +' l)) (Assoc.main n m l x y z) - ∙ sym (substCommSlice (EM ((G' ⨂ G') ⨂ G')) _ + ∙ sym (substCommSlice (EM ((G' ⨂ G') ⨂ G')) _ (EMTensorMult3ₗ) (+'-assoc n m l) (inducedFun-EM (GroupEquiv→GroupHom ⨂assoc) @@ -180,7 +180,7 @@ → x ⌣ₖ y ≡ subst (EM G') (+'-comm m n) (-ₖ^[ n · m ] (y ⌣ₖ x)) ⌣ₖ-comm n m x y = cong (EMTensorMult (n +' m)) (⌣ₖ⊗-comm n m x y) - ∙ sym (substCommSlice (EM (G' ⨂ G')) (EM G') + ∙ sym (substCommSlice (EM (G' ⨂ G')) (EM G') EMTensorMult (+'-comm m n) (-ₖ^[ n · m ] (comm⨂-EM (m +' n) (y ⌣ₖ⊗ x)))) ∙ cong (subst (EM G') (+'-comm m n)) diff --git a/Cubical.Homotopy.EilenbergMacLane.GradedCommTensor.html b/Cubical.Homotopy.EilenbergMacLane.GradedCommTensor.html index f1b0e2e5ae..e094eff623 100644 --- a/Cubical.Homotopy.EilenbergMacLane.GradedCommTensor.html +++ b/Cubical.Homotopy.EilenbergMacLane.GradedCommTensor.html @@ -552,7 +552,7 @@ (cong (-ₖ^< n · m > (m +' n) p q) (cong (comm⨂-EM (m +' n)) (0ₖ-⌣ₖ m n x) ∙ Iso→EMIso∙ ⨂-comm _) ∙ -ₖ^< n · m >∙ (m +' n) p q) - ∙ substCommSlice (λ _ → EM (G' ⨂ H') (n +' m)) + ∙ substCommSlice (λ _ → EM (G' ⨂ H') (n +' m)) (EM (G' ⨂ H')) (λ n _ → 0ₖ n) (+'-comm m n) (0ₖ _) snd (cp'∙∙ n m p q) = →∙Homogeneous≡ (isHomogeneousEM _) @@ -561,7 +561,7 @@ (cong (-ₖ^< n · m > (m +' n) p q) (cong (comm⨂-EM (m +' n)) (⌣ₖ-0ₖ m n y) ∙ Iso→EMIso∙ ⨂-comm _) ∙ -ₖ^< n · m >∙ (m +' n) p q) - ∙ substCommSlice (λ _ → EM (G' ⨂ H') (n +' m)) + ∙ substCommSlice (λ _ → EM (G' ⨂ H') (n +' m)) (EM (G' ⨂ H')) (λ n _ → 0ₖ n) (+'-comm m n) (0ₖ _)) flip-⌣ₖ-comm : (n m n' m' : ℕ) (l r : ℕ) (s : l ≡ r) @@ -873,7 +873,7 @@ ∙ sym (compSubstℕ {A = EM (G' ⨂ H')} (+'-comm (suc (suc n)) 1) (+'-comm 1 (suc (suc n))) refl)) ∙ cong (subst (EM (G' ⨂ H')) (+'-comm 1 (suc (suc n)))) - (substCommSlice (EM (H' ⨂ G')) (EM (G' ⨂ H')) + (substCommSlice (EM (H' ⨂ G')) (EM (G' ⨂ H')) (λ k x → -ₖ^< suc (suc n) · 1 > k p (inr tt) (comm⨂-EM k x)) (+'-comm (suc (suc n)) 1) @@ -948,7 +948,7 @@ ∙ cong (Iso.inv (Iso→EMIso ⨂-comm (suc m +' (suc (suc n))))) (sym (-ₖ^< suc (suc n) · suc m >² _ p q _) ∙ cong (-ₖ^< suc (suc n) · suc m > _ p q) - (sym (transport⁻Transport + (sym (transport⁻Transport (λ i → EM (G' ⨂ H') (2 +ℕ (+-comm m (suc n) i))) _) ∙ cong (subst (EM (G' ⨂ H')) (cong (2 +ℕ_) (sym (+-comm m (suc n))))) @@ -1106,7 +1106,7 @@ (_⌣ₖ_ {n = suc m} {m = suc n} (EM-raw→EM H' (suc m) a) (EM-raw→EM G' (suc n) b)))))) - ∙ sym (substCommSlice (EM (G' ⨂ H')) (EM (H' ⨂ G')) + ∙ sym (substCommSlice (EM (G' ⨂ H')) (EM (H' ⨂ G')) (λ k x → Iso.inv (Iso→EMIso ⨂-comm k) (-ₖ^< suc (suc n) · suc m > k p (evenOrOdd (suc m)) x)) @@ -1216,7 +1216,7 @@ (cong (suc ∘ suc) (sym (+-suc m n))) ℕpath (cong (suc ∘ suc) (+-comm (suc m) n))) ∙ cong (transport (λ i₁ → fst (Ω (EM∙ (G' ⨂ H') (ℕpath i₁))))) - ((substCommSlice (EM (H' ⨂ G')) + ((substCommSlice (EM (H' ⨂ G')) (λ n → typ (Ω (EM∙ (G' ⨂ H') (suc n)))) (λ k x → EM→ΩEM+1 k (-ₖ^< 2 +ℕ n · 2 +ℕ m > k p q (comm⨂-EM k (-ₖ x)))) diff --git a/Cubical.Homotopy.EilenbergMacLane.Order2.html b/Cubical.Homotopy.EilenbergMacLane.Order2.html index 2f14e9763d..51f4cd98eb 100644 --- a/Cubical.Homotopy.EilenbergMacLane.Order2.html +++ b/Cubical.Homotopy.EilenbergMacLane.Order2.html @@ -133,7 +133,7 @@ λ p → (p ∙ cong ∣_∣ₕ (sym (merid ptEM-raw)) ≡ cong ∣_∣ₕ (merid ptEM-raw) ∙ sym p) h a = - toPathP (flipTransport + toPathP (flipTransport {A = λ i → Path K2 ∣ north ∣ ∣ merid a i ∣ → Type ℓ} (funExt (λ p → (((p₃ p diff --git a/Cubical.Homotopy.EilenbergMacLane.Properties.html b/Cubical.Homotopy.EilenbergMacLane.Properties.html index 4b5ec3d652..6141954641 100644 --- a/Cubical.Homotopy.EilenbergMacLane.Properties.html +++ b/Cubical.Homotopy.EilenbergMacLane.Properties.html @@ -142,7 +142,7 @@ (Square≃doubleComp (ua (rightEquiv g)) (ua (rightEquiv (g · h))) refl (ua (rightEquiv h))) (ua (rightEquiv g) ∙ ua (rightEquiv h) - ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩ + ≡⟨ (uaCompEquiv (rightEquiv g) (rightEquiv h)) ⁻¹ ⟩ ua (compEquiv (rightEquiv g) (rightEquiv h)) ≡⟨ cong ua (compRightEquiv g h) ⟩ ua (rightEquiv (g · h)) ∎) @@ -157,7 +157,7 @@ decode : (x : EM₁ Ĝ) → Codes x → embase ≡ x decode = elimSet Ĝ (λ x → isOfHLevelΠ 2 (λ c → isGroupoidEM₁ (embase) x)) - emloop λ g → ua→ λ h → emcomp h g + emloop λ g → ua→ λ h → emcomp h g decode-encode : (x : EM₁ Ĝ) (p : embase ≡ x) → decode x (encode x p) ≡ p decode-encode x p = J (λ y q → decode y (encode y q) ≡ q) @@ -168,7 +168,7 @@ encode-decode = elimProp Ĝ (λ x → isOfHLevelΠ 1 (λ c → CodesSet x .snd _ _)) λ g → encode embase (decode embase g) ≡⟨ refl ⟩ encode embase (emloop g) ≡⟨ refl ⟩ - transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩ + transport (ua (rightEquiv g)) 1g ≡⟨ uaβ (rightEquiv g) 1g ⟩ 1g · g ≡⟨ ·IdL g ⟩ g ∎ @@ -275,7 +275,7 @@ → encode' n (0ₖ (suc (suc n))) (decode' n (0ₖ (suc (suc n))) x) ≡ x encode'-decode' zero x = cong (encode' zero (0ₖ 2)) (cong-∙ ∣_∣ₕ (merid x) (sym (merid embase))) - ∙∙ substComposite (λ x → CODE zero x .fst) + ∙∙ substComposite (λ x → CODE zero x .fst) (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) embase ∙∙ (cong (subst (λ x₁ → CODE zero x₁ .fst) (λ i → ∣ merid embase (~ i) ∣ₕ)) (λ i → lUnitₖ 1 (transportRefl x i) i) @@ -283,7 +283,7 @@ encode'-decode' (suc n) = Trunc.elim (λ _ → isOfHLevelTruncPath {n = 4 + n}) λ x → cong (encode' (suc n) (0ₖ (3 + n))) (cong-∙ ∣_∣ₕ (merid x) (sym (merid north))) - ∙∙ substComposite (λ x → CODE (suc n) x .fst) + ∙∙ substComposite (λ x → CODE (suc n) x .fst) (cong ∣_∣ₕ (merid x)) (sym (cong ∣_∣ₕ (merid ptEM-raw))) (0ₖ (2 + n)) ∙∙ cong (subst (λ x₁ → CODE (suc n) x₁ .fst) (λ i → ∣ merid ptEM-raw (~ i) ∣ₕ)) (λ i → lUnitₖ (2 + n) (transportRefl ∣ x ∣ₕ i) i) @@ -416,7 +416,7 @@ (transport (λ i → Path (EM G (suc (suc n))) ∣ merid a (~ i) ∣ ∣ merid a (~ i) ∣) p)) ∙ cong (ΩEM+1→EM (suc n)) - (flipTransport + (flipTransport (((rUnit p ∙ cong (p ∙_) (sym (lCancel _))) ∙ isCommΩEM-base (suc n) ∣ south ∣ p _) diff --git a/Cubical.Homotopy.Group.Base.html b/Cubical.Homotopy.Group.Base.html index 5b657b6166..2e1500008b 100644 --- a/Cubical.Homotopy.Group.Base.html +++ b/Cubical.Homotopy.Group.Base.html @@ -707,7 +707,7 @@ (equivToIso (Ω→ (ΩTruncSwitchFun n m) .fst , isEquivΩ→ _ (compEquiv (isoToEquiv (ΩTruncSwitch {A = A} n (suc (suc m)))) - (pathToEquiv + (pathToEquiv (λ i → typ ((Ω^ n) (hLevelTrunc∙ (+-suc n (suc m) i) A)))) .snd))) ΩTruncSwitch : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ) @@ -753,7 +753,7 @@ 2TruncΩIso {A = A} (suc n) = compIso (ΩTruncSwitch (suc n) 2) - (pathToIso λ i → typ ((Ω^ suc n) (hLevelTrunc∙ (+-comm (suc n) 2 i) A))) + (pathToIso λ i → typ ((Ω^ suc n) (hLevelTrunc∙ (+-comm (suc n) 2 i) A))) hLevΩ+ : ∀ {ℓ} {A : Pointed ℓ} (n m : ℕ) → isOfHLevel (m + n) (typ A) → isOfHLevel n (typ ((Ω^ m) A)) diff --git a/Cubical.Homotopy.Hopf.html b/Cubical.Homotopy.Hopf.html index 4e4c39d136..e53c03e77c 100644 --- a/Cubical.Homotopy.Hopf.html +++ b/Cubical.Homotopy.Hopf.html @@ -146,7 +146,7 @@ pp : PathP (λ i → ua (μ-eq a) i → TotalSpaceHopfPush) inl inr - pp = ua→ {e = μ-eq a} {B = λ _ → TotalSpaceHopfPush} λ b → push (b , a) + pp = ua→ {e = μ-eq a} {B = λ _ → TotalSpaceHopfPush} λ b → push (b , a) sect : (x : _) → TotalSpaceHopfPush→TotalSpace (inv' x) ≡ x sect (north , x) = refl @@ -379,7 +379,7 @@ compIso IsoTotalSpacePush²TotalSpacePush²' (compIso IsoTotalSpacePush²'ΣPush (compIso (equivToIso (joinPushout≃join _ _)) - (pathToIso (cong (join (typ A)) + (pathToIso (cong (join (typ A)) (isoToPath IsoTotalSpaceJoin))))) diff --git a/Cubical.Homotopy.HopfInvariant.HopfMap.html b/Cubical.Homotopy.HopfInvariant.HopfMap.html index 60b6d96625..307ea201e1 100644 --- a/Cubical.Homotopy.HopfInvariant.HopfMap.html +++ b/Cubical.Homotopy.HopfInvariant.HopfMap.html @@ -337,7 +337,7 @@ ((λ i → (λ z → cong ∣_∣ₕ (merid base ∙ sym (merid (transport - (λ j → uaInvEquiv (hopfS¹.μ-eq a) (~ i) j) x))) z)) + (λ j → uaInvEquiv (hopfS¹.μ-eq a) (~ i) j) x))) z)) ∙ λ i → cong ∣_∣ₕ (merid base ∙ sym (merid (transportRefl (invEq (hopfS¹.μ-eq a) x) i)))) ∙∙ (λ i → transp (λ i₁ → Path (HubAndSpoke (Susp S¹) 3) diff --git a/Cubical.Homotopy.Loopspace.html b/Cubical.Homotopy.Loopspace.html index e1fb387287..46c91291c3 100644 --- a/Cubical.Homotopy.Loopspace.html +++ b/Cubical.Homotopy.Loopspace.html @@ -392,7 +392,7 @@ flipΩIso : {ℓ : Level} {A : Pointed ℓ} (n : ℕ) → Iso (fst ((Ω^ (suc n)) A)) (fst ((Ω^ n) (Ω A))) -flipΩIso {A = A} n = pathToIso (cong fst (flipΩPath n)) +flipΩIso {A = A} n = pathToIso (cong fst (flipΩPath n)) flipΩIso⁻pres· : {ℓ : Level} {A : Pointed ℓ} (n : ℕ) → (f g : fst ((Ω^ (suc n)) (Ω A))) diff --git a/Cubical.Homotopy.WhiteheadsLemma.html b/Cubical.Homotopy.WhiteheadsLemma.html index 6d57091dbf..609281531b 100644 --- a/Cubical.Homotopy.WhiteheadsLemma.html +++ b/Cubical.Homotopy.WhiteheadsLemma.html @@ -56,24 +56,24 @@ ∙PathP→Square : {A B C D : Pointed ℓ} (p : A ≡ C) (q : B ≡ D) (f : A →∙ B) (g : C →∙ D) → PathP (λ i → (p i) →∙ (q i)) f g - → (Iso.inv (pathToIso (λ i → fst (q i)))) + → (Iso.inv (pathToIso (λ i → fst (q i)))) ∘ (fst g) - ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) + ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) ≡ (fst f) ∙PathP→Square {A = A} {B = B} {C = C} {D = D} = J ( λ C' p → (q : B ≡ D) (f : A →∙ B) (g : C' →∙ D) → PathP (λ i → (p i) →∙ (q i)) f g - → (Iso.inv (pathToIso (λ i → fst (q i)))) + → (Iso.inv (pathToIso (λ i → fst (q i)))) ∘ (fst g) - ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) + ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) ≡ (fst f)) ( J ( λ D' q → (f : A →∙ B) (g : A →∙ D') → PathP (λ i → A →∙ (q i)) f g - → (Iso.inv (pathToIso (λ i → fst (q i)))) + → (Iso.inv (pathToIso (λ i → fst (q i)))) ∘ (fst g) - ∘ (Iso.fun (pathToIso (λ i → (fst A)))) + ∘ (Iso.fun (pathToIso (λ i → (fst A)))) ≡ (fst f)) ( λ f g r → funExt ( λ a → transportRefl (fst g (transport refl a)) diff --git a/Cubical.Modalities.Lex.html b/Cubical.Modalities.Lex.html index 4b4b65d6d8..84ec09609b 100644 --- a/Cubical.Modalities.Lex.html +++ b/Cubical.Modalities.Lex.html @@ -140,7 +140,7 @@ abstract ⟨◯⟩→◯-section : ∀ {a} → section (⟨◯⟩→◯ {a}) ⟨◯⟩←◯ - ⟨◯⟩→◯-section = transport⁻Transport (sym (⟨◯⟩-compute _ _)) + ⟨◯⟩→◯-section = transport⁻Transport (sym (⟨◯⟩-compute _ _)) module Combinators where diff --git a/Cubical.Papers.Pi4S3.html b/Cubical.Papers.Pi4S3.html index 17779b0022..9fc97ac102 100644 --- a/Cubical.Papers.Pi4S3.html +++ b/Cubical.Papers.Pi4S3.html @@ -166,9 +166,9 @@ h : π n (S₊∙ m) ≃ π' n (Unit , tt) h = compEquiv (isoToEquiv (πTruncIso n)) - (compEquiv (pathToEquiv (cong (π n) + (compEquiv (pathToEquiv (cong (π n) (ua∙ (isoToEquiv (isContr→Iso (con-lem) isContrUnit)) refl))) - (pathToEquiv (cong ∥_∥₂ (isoToPath (IsoΩSphereMap n))))) + (pathToEquiv (cong ∥_∥₂ (isoToPath (IsoΩSphereMap n))))) -- Theorem 1 (Freudenthal Suspension Theorem) open Freudenthal using (isConnectedσ) -- formalized by Evan Cavallo diff --git a/Cubical.Papers.RepresentationIndependence.html b/Cubical.Papers.RepresentationIndependence.html index 03a002f895..804ffb7811 100644 --- a/Cubical.Papers.RepresentationIndependence.html +++ b/Cubical.Papers.RepresentationIndependence.html @@ -79,7 +79,7 @@ -- 2.2 Univalence -open Univalence using (ua ; uaβ) public +open Univalence using (ua ; uaβ) public -- Sets and Propositions open Prelude using (isProp ; isSet) public diff --git a/Cubical.Papers.ZCohomology.html b/Cubical.Papers.ZCohomology.html index 2f8a6444a8..9bc747d441 100644 --- a/Cubical.Papers.ZCohomology.html +++ b/Cubical.Papers.ZCohomology.html @@ -169,7 +169,7 @@ -- 2.3 Univalence -- Univalence and the ua function respectively -open Unival using (univalence ; ua) +open Unival using (univalence ; ua) -- Glue types open Glue using (Glue) diff --git a/Cubical.Relation.Binary.Extensionality.html b/Cubical.Relation.Binary.Extensionality.html index 63d7ce9cab..30d3b640ac 100644 --- a/Cubical.Relation.Binary.Extensionality.html +++ b/Cubical.Relation.Binary.Extensionality.html @@ -13,7 +13,7 @@ module _ {ℓ ℓ'} {A : Type ℓ} (_≺_ : Rel A A ℓ') where ≡→≺Equiv : (x y : A) → x ≡ y → ∀ z → (z ≺ x) ≃ (z ≺ y) - ≡→≺Equiv _ _ p z = substEquiv (z ≺_) p + ≡→≺Equiv _ _ p z = substEquiv (z ≺_) p isWeaklyExtensional : Type _ isWeaklyExtensional = ∀ {x y} → isEquiv (≡→≺Equiv x y) diff --git a/Cubical.Structures.Function.html b/Cubical.Structures.Function.html index f7e8428e22..6fc5708efd 100644 --- a/Cubical.Structures.Function.html +++ b/Cubical.Structures.Function.html @@ -58,7 +58,7 @@ functionTransportStr {S = S} α₁ τ₁ α₂ τ₂ e f = funExt λ t → cong (equivFun (α₂ e) ∘ f) (invTransportStr α₁ τ₁ e t) - ∙ τ₂ e (f (subst⁻ S (ua e) t)) + ∙ τ₂ e (f (subst⁻ S (ua e) t)) -- Definition of structured equivalence using an action in the domain @@ -78,7 +78,7 @@ (equivΠCod λ s → compEquiv (θ₂ e) - (pathToEquiv (cong (PathP (λ i → T (ua e i)) (f s) ∘ g) (τ₁ e s)))) + (pathToEquiv (cong (PathP (λ i → T (ua e i)) (f s) ∘ g) (τ₁ e s)))) (invEquiv heteroHomotopy≃Homotopy)) funExtDepEquiv \ No newline at end of file diff --git a/Cubical.Structures.Transfer.html b/Cubical.Structures.Transfer.html index d481aa2815..ea07c7d98a 100644 --- a/Cubical.Structures.Transfer.html +++ b/Cubical.Structures.Transfer.html @@ -40,7 +40,7 @@ (e : (X , s) ≃[ ι ] (Y , t)) → (h : H X) → P Y t (equivFun (α (e .fst)) h) → P X s h transfer⁻ P α τ ι θ {X} {Y} {s} {t} e h = - subst⁻ (λ {(Z , u , h) → P Z u h}) + subst⁻ (λ {(Z , u , h) → P Z u h}) (sip (productUnivalentStr ι θ (EquivAction→StrEquiv α) (TransportStr→UnivalentStr α τ)) (X , s , h) diff --git a/Cubical.ZCohomology.CohomologyRings.CP2.html b/Cubical.ZCohomology.CohomologyRings.CP2.html index ea5eac3ec8..afa79c0b02 100644 --- a/Cubical.ZCohomology.CohomologyRings.CP2.html +++ b/Cubical.ZCohomology.CohomologyRings.CP2.html @@ -374,11 +374,11 @@ e-sect-base : (k : ℕ) → (a : coHom k CP²) → (x : partℕ k) → ℤ[x]/x³→H*-CP² [ (ϕ⁻¹ k a x) ] ≡ base k a e-sect-base k a (is0 x) = cong (base 0) (ϕ₀-sect (substG x a)) - ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) + ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) e-sect-base k a (is2 x) = cong (base 2) (ϕ₂-sect (substG x a)) - ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) + ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) e-sect-base k a (is4 x) = cong (base 4) (ϕ₄-sect (substG x a)) - ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) + ∙ sym (constSubstCommSlice (λ x → coHom x CP²) (H* CP²) base x a) e-sect-base k a (else x) = sym (base-neutral k) ∙ cong (base k) (unitGroupSEq (sym (suc-predℕ k (fst x))) (Hⁿ-CP²≅0 (predℕ k) diff --git a/Cubical.ZCohomology.CohomologyRings.CupProductProperties.html b/Cubical.ZCohomology.CohomologyRings.CupProductProperties.html index 5818ff65d1..42874a4539 100644 --- a/Cubical.ZCohomology.CohomologyRings.CupProductProperties.html +++ b/Cubical.ZCohomology.CohomologyRings.CupProductProperties.html @@ -155,11 +155,11 @@ unitGroupSEq : {n k : ℕ} → (r : suc k ≡ n) → (e : GroupIso (coHomGr (suc k) A) UnitGroup₀) → (x y : coHom n A) → x ≡ y unitGroupSEq {n} {k} (r) e x y = x - ≡⟨ sym (substSubst⁻ (λ X → coHom X A) r _) ⟩ + ≡⟨ sym (substSubst⁻ (λ X → coHom X A) r _) ⟩ substG r (substG (sym r) x) ≡⟨ cong (substG r) (isOfHLevelRetractFromIso 1 (fst e) isPropUnit _ _) ⟩ substG r (substG (sym r) y) - ≡⟨ substSubst⁻ (λ X → coHom X A) r _ ⟩ + ≡⟨ substSubst⁻ (λ X → coHom X A) r _ ⟩ y ∎ diff --git a/Cubical.ZCohomology.CohomologyRings.RP2.html b/Cubical.ZCohomology.CohomologyRings.RP2.html index 28db4a7f07..b76cb9a509 100644 --- a/Cubical.ZCohomology.CohomologyRings.RP2.html +++ b/Cubical.ZCohomology.CohomologyRings.RP2.html @@ -415,9 +415,9 @@ e-sect-base : (k : ℕ) → (a : coHom k RP²) → (x : partℕ k) → ℤ[x]/<2x,x²>→H*-RP² (ϕ⁻¹ k a x) ≡ base k a e-sect-base k a (is0 x) = cong (base 0) (ϕ₀-sect (substG x a)) - ∙ sym (constSubstCommSlice _ _ base x a) + ∙ sym (constSubstCommSlice _ _ base x a) e-sect-base k a (is2 x) = cong (base 2) (cong ϕ₂ (ψ₂-sect _) ∙ ϕ₂-sect _) - ∙ sym (constSubstCommSlice _ _ base x a) + ∙ sym (constSubstCommSlice _ _ base x a) e-sect-base k a (else x) = sym (base-neutral k) ∙ cong (base k) (unitGroupEq (Hⁿ-RP²≅0' k (fst x) (snd x)) _ _) diff --git a/Cubical.ZCohomology.CohomologyRings.S2wedgeS4.html b/Cubical.ZCohomology.CohomologyRings.S2wedgeS4.html index 9d28b54a39..43b25f9a9a 100644 --- a/Cubical.ZCohomology.CohomologyRings.S2wedgeS4.html +++ b/Cubical.ZCohomology.CohomologyRings.S2wedgeS4.html @@ -450,11 +450,11 @@ e-sect-base : (k : ℕ) → (a : coHom k S²⋁S⁴) → (x : partℕ k) → ℤ[x,y]→H*-S²⋁S⁴ (ϕ⁻¹ k a x) ≡ base k a e-sect-base k a (is0 x) = cong (base 0) (ϕ₀-sect (substG x a)) - ∙ sym (constSubstCommSlice _ _ base x a) + ∙ sym (constSubstCommSlice _ _ base x a) e-sect-base k a (is2 x) = cong (base 2) (ϕ₂-sect _) - ∙ sym (constSubstCommSlice _ _ base x a) + ∙ sym (constSubstCommSlice _ _ base x a) e-sect-base k a (is4 x) = cong (base 4) (ϕ₄-sect _) - ∙ sym (constSubstCommSlice _ _ base x a) + ∙ sym (constSubstCommSlice _ _ base x a) e-sect-base k a (else x) = sym (base-neutral k) ∙ cong (base k) (unitGroupEq (Hⁿ-S²⋁S⁴≅0-bis k x) _ _) diff --git a/Cubical.ZCohomology.CohomologyRings.Sn.html b/Cubical.ZCohomology.CohomologyRings.Sn.html index 068c118b78..daa43b9695 100644 --- a/Cubical.ZCohomology.CohomologyRings.Sn.html +++ b/Cubical.ZCohomology.CohomologyRings.Sn.html @@ -346,17 +346,17 @@ e-sect-base : (k : ℕ) → (a : coHom k (S₊ (suc n))) → (x : partℕ k) → ℤ[x]/x²→H*-Sⁿ [ (base-trad-H* k a x) ] ≡ base k a e-sect-base k a (is0 x) = cong (base 0) (ϕ₀-sect (substG x a)) - ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a) + ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a) e-sect-base k a (isSn x) = cong (base (suc n)) (ϕₙ-sect (substG x a)) - ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a) + ∙ sym (constSubstCommSlice (λ x → coHom x (S₊ (suc n))) (H* (S₊ (suc n))) base x a) e-sect-base k a (else x) = sym (base-neutral k) - ∙ constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) (0ₕ k) + ∙ constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) (0ₕ k) ∙ cong (base (suc (predℕ k))) ((isOfHLevelRetractFromIso 1 (fst (Hⁿ-Sᵐ≅0 (predℕ k) n λ p → snd x (suc-predℕ k (fst x) ∙ cong suc p))) isPropUnit _ _)) - ∙ sym (constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) a) + ∙ sym (constSubstCommSlice ((λ x → coHom x (S₊ (suc n)))) ((H* (S₊ (suc n)))) base (suc-predℕ k (fst x)) a) e-sect : (x : H* (S₊ (suc n))) → ℤ[x]/x²→H*-Sⁿ (H*-Sⁿ→ℤ[x]/x² x) ≡ x e-sect = DS-Ind-Prop.f _ _ _ _ (λ _ → isSetH* _ _) diff --git a/Cubical.ZCohomology.Groups.KleinBottle.html b/Cubical.ZCohomology.Groups.KleinBottle.html index eff6665490..981e9eb624 100644 --- a/Cubical.ZCohomology.Groups.KleinBottle.html +++ b/Cubical.ZCohomology.Groups.KleinBottle.html @@ -91,9 +91,9 @@ movePathIso : ∀ {ℓ} {A : Type ℓ} {x : A} (p q : x ≡ x) → isComm∙ (A , x) → Iso (p ∙∙ q ∙∙ p ≡ q) (p ∙ p ≡ refl) movePathIso {x = x} p q comm = - compIso (pathToIso (movePathLem p q comm)) + compIso (pathToIso (movePathLem p q comm)) (compIso (helper (p ∙ p)) - (pathToIso (movePathLem2 p q))) + (pathToIso (movePathLem2 p q))) where helper : (p : x ≡ x) → Iso (p ∙ q ≡ q) ((p ∙ q) ∙ sym q ≡ q ∙ sym q) helper p = congIso (equivToIso (_ , compPathr-isEquiv (sym q))) @@ -240,7 +240,7 @@ Iso-H²-𝕂²₂ : Iso ∥ (Σ[ p ∈ 0ₖ 2 ≡ 0ₖ 2 ] p ∙ p ≡ refl) ∥₂ ∥ Σ[ x ∈ coHomK 1 ] x +ₖ x ≡ 0ₖ 1 ∥₂ Iso-H²-𝕂²₂ = setTruncIso (Σ-cong-iso {B' = λ x → x +ₖ x ≡ 0ₖ 1} (invIso (Iso-Kn-ΩKn+1 1)) λ p → compIso (congIso (invIso (Iso-Kn-ΩKn+1 1))) - (pathToIso λ i → ΩKn+1→Kn-hom 1 p p i ≡ 0ₖ 1)) + (pathToIso λ i → ΩKn+1→Kn-hom 1 p p i ≡ 0ₖ 1)) {- Step three : ∥ Σ[ x ∈ K₁ ] x + x ≡ 0 ∥₂ ≡ Bool diff --git a/Cubical.ZCohomology.Groups.RP2.html b/Cubical.ZCohomology.Groups.RP2.html index f1824e3824..3e3412cda6 100644 --- a/Cubical.ZCohomology.Groups.RP2.html +++ b/Cubical.ZCohomology.Groups.RP2.html @@ -60,7 +60,7 @@ private pathIso : {x : A} {p : x ≡ x} → Iso (p ≡ sym p) (p ∙ p ≡ refl) pathIso {p = p} = compIso (congIso (equivToIso (_ , compPathr-isEquiv p))) - (pathToIso (cong (p ∙ p ≡_) (lCancel p))) + (pathToIso (cong (p ∙ p ≡_) (lCancel p))) --- H⁰(RP²) ≅ ℤ ---- diff --git a/Cubical.ZCohomology.Gysin.html b/Cubical.ZCohomology.Gysin.html index 6a89d88a65..4ce808e12b 100644 --- a/Cubical.ZCohomology.Gysin.html +++ b/Cubical.ZCohomology.Gysin.html @@ -247,9 +247,9 @@ , (cong (subst coHomK (sym (+'-comm n i))) (snd f) ∙ transpPres0ₖ (sym (+'-comm n i)))) (λ f → →∙Homogeneous≡ (isHomogeneousKn _) - (funExt λ x → transportTransport⁻ _ (f .fst x))) + (funExt λ x → transportTransport⁻ _ (f .fst x))) λ f → →∙Homogeneous≡ (isHomogeneousKn _) - (funExt λ x → transportTransport⁻ _ (f .fst x))) + (funExt λ x → transportTransport⁻ _ (f .fst x))) -- g is a composition of G and our two previous equivs. g≡ : (n : ℕ) (i : ℕ) → g n i ≡ λ x @@ -507,7 +507,7 @@ subst isEquiv (sym (funExt (decomposeG i n))) (compEquiv (compEquiv (G n i , isEquivG n i) (isoToEquiv (invIso (suspKn-Iso n (n +' i))))) - (pathToEquiv (λ j → S₊∙ (suc n) →∙ coHomK-ptd (+'-suc' n i (~ j)))) .snd) + (pathToEquiv (λ j → S₊∙ (suc n) →∙ coHomK-ptd (+'-suc' n i (~ j)))) .snd) isEquiv-g : (n i : ℕ) → isEquiv (g n i) isEquiv-g n i = diff --git a/Cubical.ZCohomology.Properties.html b/Cubical.ZCohomology.Properties.html index c927cd186f..818b187c33 100644 --- a/Cubical.ZCohomology.Properties.html +++ b/Cubical.ZCohomology.Properties.html @@ -343,7 +343,7 @@ decode-elim (merid a i) = hcomp (λ k → λ { (i = i0) → σ ; (i = i1) → mainPath a k}) - (funTypeTransp (Code n) (λ x → ∣ north ∣ ≡ x) (cong ∣_∣ (merid a)) σ i) + (funTypeTransp (Code n) (λ x → ∣ north ∣ ≡ x) (cong ∣_∣ (merid a)) σ i) where mainPath : (a : (S₊ (suc n))) → transport (north≡merid a) ∘ σ ∘ transport (λ i → Code n ∣ merid a (~ i) ∣) @@ -428,7 +428,7 @@ λ a → cong encode (congFunct ∣_∣ (merid a) (sym (merid (ptSn (suc n))))) ∙∙ (λ i → transport (congFunct (Code n) (cong ∣_∣ (merid a)) (cong ∣_∣ (sym (merid (ptSn (suc n))))) i) ∣ ptSn (suc n) ∣) - ∙∙ (substComposite (λ x → x) + ∙∙ (substComposite (λ x → x) (cong (Code n) (cong ∣_∣ (merid a))) (cong (Code n) (cong ∣_∣ (sym (merid (ptSn (suc n)))))) ∣ ptSn (suc n) ∣ ∙∙ cong (transport (λ i → Code n ∣ merid (ptSn (suc n)) (~ i) ∣)) @@ -668,9 +668,9 @@ Iso.fun (fst (transportCohomIso {A = A} p)) = subst (λ n → coHom n A) p Iso.inv (fst (transportCohomIso {A = A} p)) = subst (λ n → coHom n A) (sym p) Iso.rightInv (fst (transportCohomIso p)) = - transportTransport⁻ (cong (\ n → coHomGr n _ .fst) p) + transportTransport⁻ (cong (\ n → coHomGr n _ .fst) p) Iso.leftInv (fst (transportCohomIso p)) = - transportTransport⁻ (cong (\ n → coHomGr n _ .fst) (sym p)) + transportTransport⁻ (cong (\ n → coHomGr n _ .fst) (sym p)) snd (transportCohomIso {A = A} {n = n} {m = m} p) = makeIsGroupHom (λ x y → help x y p) where diff --git a/Cubical.ZCohomology.RingStructure.CohomologyRing.html b/Cubical.ZCohomology.RingStructure.CohomologyRing.html index 3be8af606a..78029e293f 100644 --- a/Cubical.ZCohomology.RingStructure.CohomologyRing.html +++ b/Cubical.ZCohomology.RingStructure.CohomologyRing.html @@ -95,7 +95,7 @@ base (n +' m) ((-ₕ^ n · m) (subst (λ n₁ → coHom n₁ A) (+'-comm m n) (b ⌣ a))) ≡⟨ sym (-^-base n m (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a))) ⟩ (-^ n · m) (base (n +' m) (subst (λ k → coHom k A) (+'-comm m n) (b ⌣ a))) - ≡⟨ cong (-^ n · m) (sym (constSubstCommSlice (λ k → coHom k A) (H* A) base (+'-comm m n) (b ⌣ a))) ⟩ + ≡⟨ cong (-^ n · m) (sym (constSubstCommSlice (λ k → coHom k A) (H* A) base (+'-comm m n) (b ⌣ a))) ⟩ (-^ n · m) (base (m +' n) (b ⌣ a)) ∎ diff --git a/Cubical.ZCohomology.RingStructure.GradedCommutativity.html b/Cubical.ZCohomology.RingStructure.GradedCommutativity.html index 887d870734..edfc7249bd 100644 --- a/Cubical.ZCohomology.RingStructure.GradedCommutativity.html +++ b/Cubical.ZCohomology.RingStructure.GradedCommutativity.html @@ -45,7 +45,7 @@ natTranspLem : ∀ {ℓ} {A B : ℕ → Type ℓ} {n m : ℕ} (a : A n) (f : (n : ℕ) → (a : A n) → B n) (p : n ≡ m) → f m (subst A p a) ≡ subst B p (f n a) -natTranspLem {A = A} {B = B} a f p = sym (substCommSlice A B f p a) +natTranspLem {A = A} {B = B} a f p = sym (substCommSlice A B f p a) transp0₁ : (n : ℕ) → subst coHomK (+'-comm 1 (suc n)) (0ₖ _) ≡ 0ₖ _ transp0₁ zero = refl @@ -423,7 +423,7 @@ ∙∙ cong (transport (λ i → refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) i)} ≡ refl {x = 0ₖ ((+'-comm (suc (suc m)) (suc (suc n))) i)})) (natTranspLem {A = coHomK} x (λ _ → Kn→Ω²Kn+2) (cong suc (+-comm (suc n) m))) - ∙∙ sym (substComposite (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n}) + ∙∙ sym (substComposite (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n}) (cong (suc ∘ suc ∘ suc) (+-comm (suc n) m)) (+'-comm (suc (suc m)) (suc (suc n))) (Kn→Ω²Kn+2 x)) ∙∙ (λ k → subst (λ n → refl {x = 0ₖ n} ≡ refl {x = 0ₖ n}) @@ -594,7 +594,7 @@ ∙ cong (-ₖ'-gen (suc (suc n)) (suc (suc m)) p q ∘ -ₖ'-gen (suc m) (suc (suc n)) (evenOrOdd (suc m)) p ∘ -ₖ'-gen (suc n) (suc m) (evenOrOdd (suc n)) (evenOrOdd (suc m))) - (sym (substComposite coHomK (+'-comm (suc m) (suc n)) ((cong suc (sym (+-suc n m)))) x) + (sym (substComposite coHomK (+'-comm (suc m) (suc n)) ((cong suc (sym (+-suc n m)))) x) ∙ λ k → subst coHomK (isSetℕ _ _ (+'-comm (suc m) (suc n) ∙ cong suc (sym (+-suc n m))) ((cong suc (+-comm (suc m) n))) k) x) @@ -852,7 +852,7 @@ (sym (transportRefl _) ∙ (λ i → subst coHomK (isSetℕ _ _ refl (+'-comm 1 (suc (suc m)) ∙ +'-comm (suc (suc m)) 1) i) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ))) - ∙∙ substComposite coHomK + ∙∙ substComposite coHomK (+'-comm 1 (suc (suc m))) (+'-comm (suc (suc m)) 1) ((∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ)) @@ -866,7 +866,7 @@ ∙∙ sym (-ₖ^2 (subst coHomK (+'-comm 1 (suc (suc m)) ∙ +'-comm (suc (suc m)) 1) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ)))) ∙∙ (λ i → -ₖ'-gen-inr≡-ₖ' 1 (suc (suc m)) tt x (-ₖ'-gen-inr≡-ₖ' (suc (suc m)) 1 x tt - (substComposite coHomK (+'-comm 1 (suc (suc m))) (+'-comm (suc (suc m)) 1) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ) i) + (substComposite coHomK (+'-comm 1 (suc (suc m))) (+'-comm (suc (suc m)) 1) (∣ a ∣ₕ ⌣ₖ ∣ b ∣ₕ) i) (~ i)) (~ i)) ∙∙ λ i → (-ₖ'-gen 1 (suc (suc m)) (inr tt) (inr x) (transp (λ j → coHomK ((+'-comm (suc (suc m)) 1) (j ∨ ~ i))) (~ i)