From 5393766a47eba45311aeceb24a4ddb7d709ee677 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 14:28:32 +0200 Subject: [PATCH 01/13] Being n-connected is a proposition --- Cubical/Homotopy/Connected.agda | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 922a257fe4..4cc33a833a 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -40,7 +40,7 @@ open import Cubical.Homotopy.Loopspace private variable ℓ : Level - X₀ X₁ X₂ Y₀ Y₁ Y₂ : Type ℓ + A X₀ X₁ X₂ Y₀ Y₁ Y₂ : Type ℓ -- Note that relative to most sources, this notation is off by +2 isConnected : ∀ {ℓ} (n : HLevel) (A : Type ℓ) → Type ℓ @@ -98,12 +98,16 @@ isConnected→isConnectedFun : {X : Type ℓ} (n : HLevel) → isConnected n X → isConnectedFun n (λ (_ : X) → tt) isConnected→isConnectedFun n h = λ { tt → subst (isConnected n) (typeToFiber _) h } +-- Being a connected type is a proposition. +isPropIsConnected : ∀ {n : ℕ} → isProp (isConnected n A) +isPropIsConnected {A = A} {n = n} = isPropIsContr {A = hLevelTrunc n A} + isOfHLevelIsConnectedStable : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isOfHLevel n (isConnected n A) isOfHLevelIsConnectedStable {A = A} zero = (tt* , (λ _ → refl)) , λ _ → refl isOfHLevelIsConnectedStable {A = A} (suc n) = - isProp→isOfHLevelSuc n isPropIsContr + isProp→isOfHLevelSuc n isPropIsConnected module elim {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where private From 2931d1af50240ca656fa50dc90018e15bc0bc6c8 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 15:55:42 +0200 Subject: [PATCH 02/13] Being an n-connected function is a proposition --- Cubical/Homotopy/Connected.agda | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 4cc33a833a..6b3b2e1d0c 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -40,7 +40,7 @@ open import Cubical.Homotopy.Loopspace private variable ℓ : Level - A X₀ X₁ X₂ Y₀ Y₁ Y₂ : Type ℓ + A B X₀ X₁ X₂ Y₀ Y₁ Y₂ : Type ℓ -- Note that relative to most sources, this notation is off by +2 isConnected : ∀ {ℓ} (n : HLevel) (A : Type ℓ) → Type ℓ @@ -102,6 +102,10 @@ isConnected→isConnectedFun n h = λ { tt → subst (isConnected n) (typeToFibe isPropIsConnected : ∀ {n : ℕ} → isProp (isConnected n A) isPropIsConnected {A = A} {n = n} = isPropIsContr {A = hLevelTrunc n A} +-- Being a connected function is a proposition. +isPropIsConnectedFun : ∀ {n : HLevel} {f : A → B} → isProp (isConnectedFun n f) +isPropIsConnectedFun = isPropΠ λ _ → isPropIsConnected + isOfHLevelIsConnectedStable : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isOfHLevel n (isConnected n A) isOfHLevelIsConnectedStable {A = A} zero = From 1ba694362f1b96ce6ac432bec49dfcf90ded23c5 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 14:28:52 +0200 Subject: [PATCH 03/13] A type is n-connected iff every map to an n-type is constant This implements the "only if" part of Corollary 7.5.9 of the HoTT book. --- Cubical/Homotopy/Connected.agda | 35 +++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 6b3b2e1d0c..8c269a0f1c 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -12,6 +12,7 @@ open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.HLevels open import Cubical.Foundations.Path open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Structure open import Cubical.Functions.Fibration open import Cubical.Functions.FunExtEquiv @@ -230,6 +231,40 @@ indMapEquiv→conType {A = A} (suc n) BEq = , λ a → equiv-proof (BEq (P tt)) a .fst .snd) tt) +conType→indMapEquiv : ∀ (n : HLevel) + → isConnected n A + → isOfHLevel n B + → isEquiv (λ (b : B) → λ (a : A) → b) +conType→indMapEquiv {A = A} {B = B} 0 _ is-contr-B = isoToIsEquiv (isContr→Iso' is-contr-B (isContrΠ λ _ → is-contr-B) (λ b a → b)) +conType→indMapEquiv {A = A} {B = B} n@(suc _) conn-A is-of-hlevel-B = subst isEquiv fun-equiv≡const (equivIsEquiv fun-equiv) where + fun-equiv : B ≃ (A → B) + fun-equiv = + B ≃⟨ invEquiv $ Π-contractDom conn-A ⟩ + (∥ A ∥ n → B) ≃⟨ isoToEquiv (univTrunc n {B = B , is-of-hlevel-B}) ⟩ + (A → B) ■ + + fun-equiv≡const : equivFun fun-equiv ≡ (λ b a → b) + fun-equiv≡const = funExt λ b → funExt λ a → transportRefl b + +-- Corollary 7.5.9 of the HoTT book: +-- A type is n-connected if and only every map into an n-type is constant. +indMapEquiv≃conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel) + → ((B : TypeOfHLevel ℓ n) → isEquiv (λ (b : ⟨ B ⟩) → λ (a : A) → b)) + ≃ + isConnected n A +indMapEquiv≃conType n = propBiimpl→Equiv + (isPropΠ λ B → isPropIsEquiv (λ b a → b)) + (isPropIsConnected) + (indMapEquiv→conType n) + (λ conn-A (B , is-of-hlevel-B) → conType→indMapEquiv n conn-A is-of-hlevel-B) + +isConnected→constEquiv : ∀ (n : HLevel) + → isConnected n A + → isOfHLevel n B + → B ≃ (A → B) +isConnected→constEquiv n conn-A is-of-hlevel-B .fst = λ b a → b +isConnected→constEquiv n conn-A is-of-hlevel-B .snd = conType→indMapEquiv n conn-A is-of-hlevel-B + isConnectedComp : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (f : B → C) (g : A → B) (n : ℕ) → isConnectedFun n f From a07f49a3e7ee3bf8a1a60578ae551d6e33add0da Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 14:46:49 +0200 Subject: [PATCH 04/13] All k-connected k-types are are contractible --- Cubical/Homotopy/Connected.agda | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 8c269a0f1c..bc4756b553 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -114,6 +114,20 @@ isOfHLevelIsConnectedStable {A = A} zero = isOfHLevelIsConnectedStable {A = A} (suc n) = isProp→isOfHLevelSuc n isPropIsConnected +-- A k-connected k-type is contractible. +isOfHLevel×isConnected→isContr : ∀ {ℓ} (k : HLevel) + → (A : Type ℓ) + → (isOfHLevel k A) + → (isConnected k A) + → isContr A +isOfHLevel×isConnected→isContr zero A is-contr-A _ = is-contr-A +isOfHLevel×isConnected→isContr (suc k) A is-trunc-A is-conn-A = is-contr-A where + universal-property-trunc : ∥ A ∥ suc k ≃ A + universal-property-trunc = truncIdempotent≃ (suc k) is-trunc-A + + is-contr-A : isContr A + is-contr-A = isOfHLevelRespectEquiv 0 universal-property-trunc is-conn-A + module elim {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) where private inv : ∀ {ℓ'''} (n : HLevel) (P : B → TypeOfHLevel ℓ''' (suc n)) From c74a2e326f227f1ae988a378a6175e30e076a571 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 15:43:25 +0200 Subject: [PATCH 05/13] A type is (k+1)-connected iff it is merely inhabited and has k-connected paths This implements Exercise 7.6 of the HoTT book. --- Cubical/Homotopy/Connected.agda | 45 +++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index bc4756b553..bbb8a7c7a4 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -35,6 +35,7 @@ open import Cubical.HITs.Sn.Base open import Cubical.HITs.S1 hiding (elim) open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec) hiding (elim) +open import Cubical.HITs.PropositionalTruncation as PT using (∥_∥₁) open import Cubical.Homotopy.Loopspace @@ -496,6 +497,50 @@ isConnectedRetractFromIso n e = (Iso.inv e) (Iso.leftInv e) +-- Any (k+1)-connected type is (merely) inhabited. +isConnectedSuc→merelyInh : ∀ (k : HLevel) → isConnected (suc k) A → ∥ A ∥₁ +isConnectedSuc→merelyInh {A = A} k conn-A = propTruncTrunc1Iso .Iso.inv (is-1-conn-A .fst) where + is-1-conn-A : isConnected 1 A + is-1-conn-A = isConnectedSubtr' k 1 conn-A + +-- A pointed type with k-connected path space is (k+1)-connected. +pointed×isConnectedPath→isConnectedSuc : ∀ (k : HLevel) → (a : A) → ((a b : A) → isConnected k (a ≡ b)) → isConnected (suc k) A +pointed×isConnectedPath→isConnectedSuc {A = A} k a conn-path = conn where + is-of-hlevel-trunc : isOfHLevel (2 + k) (∥ A ∥ (suc k)) + is-of-hlevel-trunc = isOfHLevelSuc (1 + k) (isOfHLevelTrunc (1 + k)) + + conn : isConnected (suc k) A + conn .fst = ∣ a ∣ₕ + conn .snd = Trunc.elim + (λ y → is-of-hlevel-trunc ∣ a ∣ y) + (λ b → PathIdTruncIso k .Iso.inv (conn-path a b .fst)) + +-- A merely inhabited type with k-connected path space is (k+1)-connected. +merelyInh×isConnectedPath→isConnectedSuc : ∀ (k : HLevel) + → ∥ A ∥₁ + → ((a b : A) → isConnected k (a ≡ b)) + → isConnected (suc k) A +merelyInh×isConnectedPath→isConnectedSuc k = PT.rec + (isProp→ isPropIsConnected) + (pointed×isConnectedPath→isConnectedSuc k) + +-- The converse: A (k+1)-connected type is merely inhabited and has k-connected paths. +isConnectedSuc→merelyInh×isConnectedPath : (k : HLevel) + → isConnected (suc k) A + → ∥ A ∥₁ × ((a b : A) → isConnected k (a ≡ b)) +isConnectedSuc→merelyInh×isConnectedPath k suc-conn-A .fst = isConnectedSuc→merelyInh k suc-conn-A +isConnectedSuc→merelyInh×isConnectedPath k suc-conn-A .snd = isConnectedPath k suc-conn-A + +-- HoTT book, Exercise 7.6: +-- A type is k+1-connected whenever it is merely inhabited and has k-connected paths. +merelyInh×isConnectedPath≃isConnectedSuc : ∀ {ℓ} {A : Type ℓ} (k : HLevel) + → (∥ A ∥₁ × ((a b : A) → isConnected k (a ≡ b))) ≃ (isConnected (suc k) A) +merelyInh×isConnectedPath≃isConnectedSuc k = propBiimpl→Equiv + (isProp× PT.isPropPropTrunc $ isPropΠ2 λ a b → isPropIsConnected) + isPropIsConnected + (uncurry $ merelyInh×isConnectedPath→isConnectedSuc k) + (isConnectedSuc→merelyInh×isConnectedPath k) + isConnectedPoint : ∀ {ℓ} (n : HLevel) {A : Type ℓ} → isConnected (suc n) A → (a : A) → isConnectedFun n (λ(_ : Unit) → a) From 3a88b4d4a165c22ff09387cca4e7c4daa3770ab1 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 18:08:14 +0200 Subject: [PATCH 06/13] A type is (k+1)-connected iff it is (k+1)-inhabited and has k-connected paths --- Cubical/Homotopy/Connected.agda | 51 +++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index bbb8a7c7a4..5f1e2dd7b9 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -541,6 +541,57 @@ merelyInh×isConnectedPath≃isConnectedSuc k = propBiimpl→Equiv (uncurry $ merelyInh×isConnectedPath→isConnectedSuc k) (isConnectedSuc→merelyInh×isConnectedPath k) +-- If a type is (k+1)-inhabited and has k-connected paths, then it is (k+1)-connected. +inhTruncSuc×isConnectedPath→isConnectedSuc : ∀ (k : HLevel) + → ∥ A ∥ (suc k) + → ((a b : A) → isConnected k (a ≡ b)) + → isConnected (suc k) A +inhTruncSuc×isConnectedPath→isConnectedSuc k = Trunc.rec + (isOfHLevelΠ (suc k) λ _ → isProp→isOfHLevelSuc k isPropIsConnected) + (pointed×isConnectedPath→isConnectedSuc k) + +-- A type is (k+1)-inhabited and has k-connected paths if and only if it is (k+1)-connected. +-- +-- Note that the left hand side of the equivalence is not a priori a proposition. +inhTruncSuc×isConnectedPath≃isConnectedSuc : ∀ (k : HLevel) + → (∥ A ∥ (suc k) × ((a b : A) → isConnected k (a ≡ b))) ≃ (isConnected (suc k) A) +inhTruncSuc×isConnectedPath≃isConnectedSuc {A = A} k = equiv where + -- The left-to-right implication has been established above. + impl : (∥ A ∥ (suc k) × ((a b : A) → isConnected k (a ≡ b))) → (isConnected (suc k) A) + impl = uncurry (inhTruncSuc×isConnectedPath→isConnectedSuc k) + + -- Even though ∥ A ∥ₖ₊₁ is not a proposition in general, we know that this is the + -- case whenever A is (k+1)-connected. We can thus prove that fibers of the above + -- implication are contractible, since we get to assume (k+1)-connectedness of A: + is-contr-fiber-impl : (suc-conn-A : isConnected (suc k) A) → isContr (fiber impl suc-conn-A) + is-contr-fiber-impl suc-conn-A = goal where + -- (1). By assumption, having k-connected paths is an inhabited proposition, i.e. contractible. + is-contr-is-conn-path : isContr (∀ (a b : A) → isConnected k (a ≡ b)) + is-contr-is-conn-path = inhProp→isContr (isConnectedPath k suc-conn-A) (isPropΠ2 λ _ _ → isPropIsConnected) + + -- (2). Being (k+1)-connected means that ∥ A ∥ₖ₊₁ is contractible. + -- Together with (1), it follows that the domain of the implication is contractible. + is-contr-trunc×conn-path : isContr (∥ A ∥ (suc k) × ∀ (a b : A) → isConnected k (a ≡ b)) + is-contr-trunc×conn-path = isContrΣ suc-conn-A λ _ → is-contr-is-conn-path + + -- (3). The codomain is a proposition, so its paths are contractible. As such, there is a unique homotopy + -- connecting points in the image of `impl` to our assumption of connectedness of A. + is-contr-impl-conn-path : (trunc×conn : (∥ A ∥ suc k) × (∀ a b → isConnected k (a ≡ b))) → isContr (impl trunc×conn ≡ suc-conn-A) + is-contr-impl-conn-path trunc×conn = isProp→isContrPath isPropIsConnected (impl trunc×conn) suc-conn-A + + -- Together, (2) and (3) say that `impl` has contractible fibers. + goal : isContr (fiber impl suc-conn-A) + goal = isContrΣ is-contr-trunc×conn-path is-contr-impl-conn-path + + equiv : _ ≃ _ + equiv .fst = impl + equiv .snd .equiv-proof = is-contr-fiber-impl + +isConnectedSuc→inhTruncSuc×isConnectedPath : ∀ (k : HLevel) + → (isConnected (suc k) A) + → (∥ A ∥ (suc k) × ((a b : A) → isConnected k (a ≡ b))) +isConnectedSuc→inhTruncSuc×isConnectedPath k = invEq $ inhTruncSuc×isConnectedPath≃isConnectedSuc k + isConnectedPoint : ∀ {ℓ} (n : HLevel) {A : Type ℓ} → isConnected (suc n) A → (a : A) → isConnectedFun n (λ(_ : Unit) → a) From d19848c8582f50f7c37093a1585f0c14ecd5cef6 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Tue, 18 Feb 2025 18:03:15 +0200 Subject: [PATCH 07/13] All loop spaces of a (k+2)-connected type are merely equivalent --- Cubical/Homotopy/Connected.agda | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 5f1e2dd7b9..99c29827a6 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -592,6 +592,19 @@ isConnectedSuc→inhTruncSuc×isConnectedPath : ∀ (k : HLevel) → (∥ A ∥ (suc k) × ((a b : A) → isConnected k (a ≡ b))) isConnectedSuc→inhTruncSuc×isConnectedPath k = invEq $ inhTruncSuc×isConnectedPath≃isConnectedSuc k +-- In a (k+2)-connected space, all loop spaces are merely equivalent +isConnected→mereLoopSpaceEquiv : (k : HLevel) → isConnected (2 + k) A → (a b : A) → ∥ (a ≡ a) ≃ (b ≡ b) ∥₁ +isConnected→mereLoopSpaceEquiv {A = A} k conn-A a b = do + -- Paths in A are (k+1)-connected: + let conn-path-A : (a b : A) → isConnected (suc k) (a ≡ b) + conn-path-A = isConnectedPath (suc k) conn-A + -- Therefore, there merely exists a path a ≡ b: + a≡b ← isConnectedSuc→merelyInh k (conn-path-A a b) + -- Conjugation by this path induces an equivance of loop spaces + return (conjugatePathEquiv a≡b) + where + open import Cubical.HITs.PropositionalTruncation.Monad + isConnectedPoint : ∀ {ℓ} (n : HLevel) {A : Type ℓ} → isConnected (suc n) A → (a : A) → isConnectedFun n (λ(_ : Unit) → a) From f0a56d94c46cb73631a7f9e719aba829e88e68ba Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Thu, 27 Feb 2025 12:55:59 +0200 Subject: [PATCH 08/13] =?UTF-8?q?Avoid=20univalence=20in=20proof=20of=20`i?= =?UTF-8?q?sConnectedFun=E2=86=92isConnected`=20and=20converse?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/Homotopy/Connected.agda | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 99c29827a6..540e2a8993 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -91,14 +91,23 @@ private typeToFiber : ∀ {ℓ} (A : Type ℓ) → A ≡ fiber (λ (x : A) → tt) tt typeToFiber A = isoToPath (typeToFiberIso A) +private + truncTypeToFiberIso : (n : HLevel) (X : Type ℓ) → Iso (∥ X ∥ n) (∥ fiber (λ x → tt) tt ∥ n) + truncTypeToFiberIso n X = mapCompIso {n = n} (typeToFiberIso X) + isConnectedFun→isConnected : {X : Type ℓ} (n : HLevel) → isConnectedFun n (λ (_ : X) → tt) → isConnected n X -isConnectedFun→isConnected n h = - subst (isConnected n) (sym (typeToFiber _)) (h tt) +isConnectedFun→isConnected {X = X} zero _ = isConnectedZero X +isConnectedFun→isConnected {X = X} n@(suc _) h = + isOfHLevelRetractFromIso 0 (truncTypeToFiberIso n X) is-contr-fiber + where + is-contr-fiber : isContr (∥ fiber (λ (_ : X) → tt) tt ∥ n) + is-contr-fiber = h tt isConnected→isConnectedFun : {X : Type ℓ} (n : HLevel) → isConnected n X → isConnectedFun n (λ (_ : X) → tt) -isConnected→isConnectedFun n h = λ { tt → subst (isConnected n) (typeToFiber _) h } +isConnected→isConnectedFun {X = X} zero h = isConnectedZero ∘ fiber {A = X} (λ _ → tt) +isConnected→isConnectedFun {X = X} n@(suc _) h tt = isOfHLevelRetractFromIso 0 (invIso (truncTypeToFiberIso n X)) h -- Being a connected type is a proposition. isPropIsConnected : ∀ {n : ℕ} → isProp (isConnected n A) From 86b868a0d5a64ff53d81f5720d7df191106b37de Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Thu, 27 Feb 2025 13:01:35 +0200 Subject: [PATCH 09/13] =?UTF-8?q?Restructure=20proof=20of=20`indMapEquiv?= =?UTF-8?q?=E2=86=92conType`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The proof was essentially an application of `isConnectedFun→isConnected` in disguise. The new proof hopefully makes it clear how the elimination principle for connected connected functions is applied. --- Cubical/Homotopy/Connected.agda | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 540e2a8993..c059a2081a 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -247,13 +247,27 @@ indMapEquiv→conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel) → ((B : TypeOfHLevel ℓ n) → isEquiv (λ (b : (fst B)) → λ (a : A) → b)) → isConnected n A -indMapEquiv→conType {A = A} zero BEq = isContrUnit* -indMapEquiv→conType {A = A} (suc n) BEq = - isOfHLevelRetractFromIso 0 (mapCompIso {n = (suc n)} (typeToFiberIso A)) - (elim.isConnectedPrecompose (λ _ → tt) (suc n) - (λ P → ((λ a _ → a) ∘ invIsEq (BEq (P tt))) - , λ a → equiv-proof (BEq (P tt)) a .fst .snd) - tt) +indMapEquiv→conType {A = A} zero _ = isConnectedZero A +indMapEquiv→conType {A = A} (suc n) is-equiv-ind = + isConnectedFun→isConnected (suc n) is-conn-fun-const + where + module _ (P : Unit → TypeOfHLevel _ (suc n)) where + B' : Type _ + B' = ⟨ P tt ⟩ + + B-equiv : B' ≃ (A → B') + B-equiv .fst = λ b a → b + B-equiv .snd = is-equiv-ind (P tt) + + precomp-section : ((a : A) → B') → (b : Unit) → B' + precomp-section = (λ b (_ : Unit) → b) ∘ invEq B-equiv + + has-section : hasSection (λ s → s ∘ (λ (a : A) → tt)) + has-section .fst = precomp-section + has-section .snd = secEq B-equiv + + is-conn-fun-const : isConnectedFun (suc n) (λ (a : A) → tt) + is-conn-fun-const = elim.isConnectedPrecompose _ _ has-section conType→indMapEquiv : ∀ (n : HLevel) → isConnected n A From dd4de3bf6ab78d61edbf183649ff76cc0911e1ed Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Thu, 27 Feb 2025 13:20:54 +0200 Subject: [PATCH 10/13] =?UTF-8?q?Strengthen=20`indMapEquiv=E2=86=92conType?= =?UTF-8?q?`=20to=20only=20require=20existence=20of=20a=20section?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/Homotopy/Connected.agda | 35 +++++++++++++++++++++------------ 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index c059a2081a..87732d4c72 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -243,31 +243,40 @@ isOfHLevelPrecomposeConnected (suc k) n P f fConn t = f fConn (funExt⁻ (p₀ ∙∙ refl ∙∙ sym p₁)))))} -indMapEquiv→conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel) - → ((B : TypeOfHLevel ℓ n) - → isEquiv (λ (b : (fst B)) → λ (a : A) → b)) +-- A type A is n-connected if the map `λ b a → b : B → (A → B)` has a section for any n-type B. +indMapHasSection→conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel) + → ((B : TypeOfHLevel ℓ n) → hasSection (λ (b : (fst B)) → λ (a : A) → b)) → isConnected n A -indMapEquiv→conType {A = A} zero _ = isConnectedZero A -indMapEquiv→conType {A = A} (suc n) is-equiv-ind = +indMapHasSection→conType {A = A} zero _ = isConnectedZero A +indMapHasSection→conType {A = A} (suc n) ind-map-has-section = isConnectedFun→isConnected (suc n) is-conn-fun-const where module _ (P : Unit → TypeOfHLevel _ (suc n)) where B' : Type _ B' = ⟨ P tt ⟩ - B-equiv : B' ≃ (A → B') - B-equiv .fst = λ b a → b - B-equiv .snd = is-equiv-ind (P tt) + has-section : hasSection λ (b : B') (a : A) → b + has-section = ind-map-has-section (P tt) + + point : (A → B') → B' + point = has-section .fst precomp-section : ((a : A) → B') → (b : Unit) → B' - precomp-section = (λ b (_ : Unit) → b) ∘ invEq B-equiv + precomp-section = (λ b (_ : Unit) → b) ∘ point - has-section : hasSection (λ s → s ∘ (λ (a : A) → tt)) - has-section .fst = precomp-section - has-section .snd = secEq B-equiv + precomp-has-section : hasSection (λ s → s ∘ (λ (a : A) → tt)) + precomp-has-section .fst = precomp-section + precomp-has-section .snd = has-section .snd is-conn-fun-const : isConnectedFun (suc n) (λ (a : A) → tt) - is-conn-fun-const = elim.isConnectedPrecompose _ _ has-section + is-conn-fun-const = elim.isConnectedPrecompose _ _ precomp-has-section + +-- Corollary: A is n-connected if the constant map `B → (A → B)` is an equivalence for any n-type B. +indMapEquiv→conType : ∀ {ℓ} {A : Type ℓ} (n : HLevel) + → ((B : TypeOfHLevel ℓ n) + → isEquiv (λ (b : (fst B)) → λ (a : A) → b)) + → isConnected n A +indMapEquiv→conType n is-equiv-ind = indMapHasSection→conType n λ B → _ , secIsEq (is-equiv-ind B) conType→indMapEquiv : ∀ (n : HLevel) → isConnected n A From 99c3eae3c3e5ae8252a1620c7ccd43ca6ef595a3 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Mon, 10 Mar 2025 10:32:04 +0200 Subject: [PATCH 11/13] A pointed type is connected iff all points merely have a path to the base --- Cubical/Homotopy/Connected.agda | 39 +++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 87732d4c72..0c7d537412 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -573,6 +573,45 @@ merelyInh×isConnectedPath≃isConnectedSuc k = propBiimpl→Equiv (uncurry $ merelyInh×isConnectedPath→isConnectedSuc k) (isConnectedSuc→merelyInh×isConnectedPath k) +module Pointed {ℓ} (A : Pointed ℓ) where + private + a₀ : ⟨ A ⟩ + a₀ = str A + + -- A pointed type has k-connected path space iff it is (k+1)-connected. + isConnectedPath≃isConnectedSuc : ∀ (k : HLevel) + → ((a b : ⟨ A ⟩) → isConnected k (a ≡ b)) ≃ (isConnected (suc k) ⟨ A ⟩) + isConnectedPath≃isConnectedSuc k = propBiimpl→Equiv + (isPropΠ2 λ a b → isPropIsConnected) + (isPropIsConnected) + (pointed×isConnectedPath→isConnectedSuc k a₀) + (isConnectedPath k) + + merePathToBase→isConnectedPath : (∀ x → ∥ x ≡ a₀ ∥₁) → ∀ (a b : ⟨ A ⟩) → isConnected 1 (a ≡ b) + merePathToBase→isConnectedPath to-base a b = + inhProp→isContr (propTruncTrunc1Iso .Iso.fun mere-path) (isOfHLevelTrunc 1) where + open import Cubical.HITs.PropositionalTruncation.Monad + + mere-path : ∥ a ≡ b ∥₁ + mere-path = do + a≡a₀ ← to-base a + b≡a₀ ← to-base b + return (a≡a₀ ∙ sym b≡a₀) + + isConnectedPath→merePathToBase : (∀ (a b : ⟨ A ⟩) → isConnected 1 (a ≡ b)) → (∀ x → ∥ x ≡ a₀ ∥₁) + isConnectedPath→merePathToBase is-conn-path x = isConnectedSuc→merelyInh 0 (is-conn-path x a₀) + + merePathToBase≃isConnectedPath : (∀ x → ∥ x ≡ a₀ ∥₁) ≃ (∀ (a b : ⟨ A ⟩) → isConnected 1 (a ≡ b)) + merePathToBase≃isConnectedPath = propBiimpl→Equiv + (isPropΠ λ x → PT.isPropPropTrunc) + (isPropΠ2 λ a b → isPropIsConnected) + merePathToBase→isConnectedPath + isConnectedPath→merePathToBase + + -- In a pointed type, each point merely has a path to the base point iff the type is 2-connected. + merePathToBase≃is2Connected : (∀ x → ∥ x ≡ a₀ ∥₁) ≃ isConnected 2 ⟨ A ⟩ + merePathToBase≃is2Connected = merePathToBase≃isConnectedPath ∙ₑ isConnectedPath≃isConnectedSuc 1 + -- If a type is (k+1)-inhabited and has k-connected paths, then it is (k+1)-connected. inhTruncSuc×isConnectedPath→isConnectedSuc : ∀ (k : HLevel) → ∥ A ∥ (suc k) From b070044fb5680f6c9d96ba515a46d7bde38f4ed0 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Fri, 21 Mar 2025 14:40:09 +0200 Subject: [PATCH 12/13] Promote some isomorphisms of truncations to equivalences --- Cubical/HITs/Truncation/Properties.agda | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Cubical/HITs/Truncation/Properties.agda b/Cubical/HITs/Truncation/Properties.agda index 7f89a76036..3edd5dda09 100644 --- a/Cubical/HITs/Truncation/Properties.agda +++ b/Cubical/HITs/Truncation/Properties.agda @@ -316,6 +316,9 @@ Iso.inv (mapCompIso {n = (suc n)} g) = map (Iso.inv g) Iso.rightInv (mapCompIso {n = (suc n)} g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ b → cong ∣_∣ (Iso.rightInv g b) Iso.leftInv (mapCompIso {n = (suc n)} g) = elim (λ x → isOfHLevelPath _ (isOfHLevelTrunc _) _ _) λ a → cong ∣_∣ (Iso.leftInv g a) +mapCompEquiv : {n : HLevel} {B : Type ℓ'} → (A ≃ B) → (hLevelTrunc n A) ≃ (hLevelTrunc n B) +mapCompEquiv e = isoToEquiv (mapCompIso (equivToIso e)) + mapId : {n : HLevel} → ∀ t → map {n = n} (idfun A) t ≡ t mapId {n = 0} tt* = refl mapId {n = (suc n)} = @@ -576,6 +579,10 @@ Iso.rightInv (truncOfΣIso (suc n)) = Iso.leftInv (truncOfΣIso (suc n)) = elim (λ _ → isOfHLevelPath (suc n) (isOfHLevelTrunc (suc n)) _ _) λ {(a , b) → refl} +truncOfΣEquiv : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : A → Type ℓ'} + → (hLevelTrunc n (Σ A B)) ≃ (hLevelTrunc n (Σ A (hLevelTrunc n ∘ B))) +truncOfΣEquiv n = isoToEquiv (truncOfΣIso n) + {- transport along family of truncations -} transportTrunc : {n : HLevel}{p : A ≡ B} From ebb27bc995a5c40dae60d92ae7137398307b8934 Mon Sep 17 00:00:00 2001 From: Philipp Joram Date: Fri, 21 Mar 2025 14:40:41 +0200 Subject: [PATCH 13/13] =?UTF-8?q?Connected=20types=20are=20closed=20under?= =?UTF-8?q?=20`=CE=A3`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Cubical/Homotopy/Connected.agda | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 0c7d537412..24c11f11b5 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -460,6 +460,17 @@ isConnectedCong' {x = x} n f conf p = → doubleCompPath-filler (sym p) (cong f q) p i)) (isConnectedCong n f conf) +isConnectedΣ : ∀ {ℓA ℓB} {A : Type ℓA} {B : A → Type ℓB} (k : HLevel) + → isConnected k A + → (∀ a → isConnected k (B a)) + → isConnected k (Σ A B) +isConnectedΣ {A = A} {B = B} k is-conn-A is-conn-B = isOfHLevelRespectEquiv 0 (invEquiv contr-equiv) is-conn-A where + contr-equiv : ∥ Σ A B ∥ k ≃ ∥ A ∥ k + contr-equiv = + ∥ Σ[ a ∈ A ] B a ∥ k ≃⟨ truncOfΣEquiv k ⟩ + ∥ Σ[ a ∈ A ] (∥ B a ∥ k) ∥ k ≃⟨ mapCompEquiv (Σ-contractSnd is-conn-B) ⟩ + ∥ A ∥ k ■ + isConnectedΩ→ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} (n : ℕ) → (f : A →∙ B) → isConnectedFun (suc n) (fst f)