From 5427228029fcd4f49cf28638835dac9082358121 Mon Sep 17 00:00:00 2001
From: Reid Barton <rwbarton@gmail.com>
Date: Mon, 2 Oct 2023 08:54:43 -0400
Subject: [PATCH] more connectivity lemmas (#1063)

---
 Cubical/Data/Prod/Properties.agda | 15 ++++++++++
 Cubical/HITs/Susp/Base.agda       | 12 ++++++++
 Cubical/Homotopy/Connected.agda   | 50 ++++++++++++++++++++++++++++++-
 3 files changed, 76 insertions(+), 1 deletion(-)

diff --git a/Cubical/Data/Prod/Properties.agda b/Cubical/Data/Prod/Properties.agda
index da8c7eed07..393352c444 100644
--- a/Cubical/Data/Prod/Properties.agda
+++ b/Cubical/Data/Prod/Properties.agda
@@ -8,6 +8,7 @@ open import Cubical.Data.Sigma renaming (_×_ to _×Σ_) hiding (prodIso ; toPro
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
@@ -109,3 +110,17 @@ Iso.fun curryIso f a b = f (a , b)
 Iso.inv curryIso f (a , b) = f a b
 Iso.rightInv curryIso a = refl
 Iso.leftInv curryIso f = funExt λ {(a , b) → refl}
+
+fiber-map-× : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+    (f : B → C) (a : A) (c : C)
+  → Iso (fiber f c) (fiber (map-× (idfun A) f) (a , c))
+fiber-map-× f a c .Iso.fun z .fst .fst = a
+fiber-map-× f a c .Iso.fun z .fst .snd = z .fst
+fiber-map-× f a c .Iso.fun z .snd = ≡-× refl (z .snd)
+fiber-map-× f a c .Iso.inv z .fst = z .fst .snd
+fiber-map-× f a c .Iso.inv z .snd = cong snd (z .snd)
+fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .fst .fst = cong fst e (~ j)
+fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .fst .snd = bz
+fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .snd k .fst = cong fst e (k ∨ ~ j)
+fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .snd k .snd = cong snd e k
+fiber-map-× f a c .Iso.leftInv z = refl
diff --git a/Cubical/HITs/Susp/Base.agda b/Cubical/HITs/Susp/Base.agda
index c9bb99c2e4..98a456bee8 100644
--- a/Cubical/HITs/Susp/Base.agda
+++ b/Cubical/HITs/Susp/Base.agda
@@ -7,6 +7,7 @@ open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Pointed
 
+open import Cubical.Data.Unit
 open import Cubical.Data.Bool
 open import Cubical.Data.Empty
 
@@ -35,6 +36,17 @@ suspFun f north = north
 suspFun f south = south
 suspFun f (merid a i) = merid (f a) i
 
+UnitIsoSuspUnit : Iso Unit (Susp Unit)
+fun UnitIsoSuspUnit _ = north
+inv UnitIsoSuspUnit _ = tt
+rightInv UnitIsoSuspUnit north = refl
+rightInv UnitIsoSuspUnit south = merid tt
+rightInv UnitIsoSuspUnit (merid tt j) k = merid tt (j ∧ k)
+leftInv UnitIsoSuspUnit _ = refl
+
+Unit≃SuspUnit : Unit ≃ Susp Unit
+Unit≃SuspUnit = isoToEquiv UnitIsoSuspUnit
+
 BoolIsoSusp⊥ : Iso Bool (Susp ⊥)
 fun BoolIsoSusp⊥ = λ {true  → north; false → south}
 inv BoolIsoSusp⊥ = λ {north → true;  south → false}
diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda
index d865dfe0dc..5640935b83 100644
--- a/Cubical/Homotopy/Connected.agda
+++ b/Cubical/Homotopy/Connected.agda
@@ -15,11 +15,15 @@ open import Cubical.Foundations.Univalence
 
 open import Cubical.Functions.Fibration
 open import Cubical.Functions.FunExtEquiv
+open import Cubical.Functions.Surjection
 
 open import Cubical.Data.Unit
-open import Cubical.Data.Bool hiding (elim)
+open import Cubical.Data.Bool hiding (elim; _≤_)
 open import Cubical.Data.Nat hiding (elim)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.NatMinusOne
 open import Cubical.Data.Sigma
+open import Cubical.Data.Prod.Properties
 
 open import Cubical.HITs.Nullification hiding (elim)
 open import Cubical.HITs.Susp
@@ -45,6 +49,9 @@ isConnected n A = isContr (hLevelTrunc n A)
 isConnectedFun : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ')
 isConnectedFun n f = ∀ b → isConnected n (fiber f b)
 
+isConnectedZero : ∀ {ℓ} (A : Type ℓ) → isConnected 0 A
+isConnectedZero A = isContrUnit*
+
 isConnectedSubtr : ∀ {ℓ} {A : Type ℓ} (n m : HLevel)
                 → isConnected (m + n) A
                 → isConnected n A
@@ -60,6 +67,12 @@ isConnectedFunSubtr : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLeve
                 → isConnectedFun n f
 isConnectedFunSubtr n m f iscon b = isConnectedSubtr n m (iscon b)
 
+isConnectedFun≤ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLevel) (f : A → B)
+  → n ≤ m → isConnectedFun m f → isConnectedFun n f
+isConnectedFun≤ n m f hnm hf =
+  isConnectedFunSubtr n (hnm .fst) f
+    (subst (λ d → isConnectedFun d f) (sym (hnm .snd)) hf)
+
 private
   typeToFiberIso : ∀ {ℓ} (A : Type ℓ) → Iso A (fiber (λ (x : A) → tt) tt)
   Iso.fun (typeToFiberIso A) x = x , refl
@@ -70,6 +83,15 @@ private
   typeToFiber : ∀ {ℓ} (A : Type ℓ) → A ≡ fiber (λ (x : A) → tt) tt
   typeToFiber A = isoToPath (typeToFiberIso A)
 
+isConnectedFun→isConnected : {X : Type ℓ} (n : HLevel)
+  → isConnectedFun n (λ (_ : X) → tt) → isConnected n X
+isConnectedFun→isConnected n h =
+  subst (isConnected n) (sym (typeToFiber _)) (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 }
+
 isOfHLevelIsConnectedStable : ∀ {ℓ} {A : Type ℓ} (n : ℕ)
   → isOfHLevel n (isConnected n A)
 isOfHLevelIsConnectedStable {A = A} zero =
@@ -284,6 +306,9 @@ isEquiv→isConnected : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
 isEquiv→isConnected f iseq n b =
   isContr→isContr∥ n (equiv-proof iseq b)
 
+isConnectedId : ∀ {ℓ} {A : Type ℓ} {n : HLevel} → isConnectedFun n (idfun A)
+isConnectedId = isEquiv→isConnected _ (idIsEquiv _) _
+
 
 isConnectedPath : ∀ {ℓ} (n : HLevel) {A : Type ℓ}
   → isConnected (suc n) A
@@ -478,6 +503,11 @@ connectedTruncEquiv : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B)
                    → hLevelTrunc n A ≃ hLevelTrunc n B
 connectedTruncEquiv {A = A} {B = B} n f con = isoToEquiv (connectedTruncIso n f con)
 
+isConnectedSuc→isSurjection : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n : HLevel}
+  → isConnectedFun (suc n) f → isSurjection f
+isConnectedSuc→isSurjection hf b =
+  Iso.inv propTruncTrunc1Iso (isConnectedFun≤ 1 _ _ (suc-≤-suc zero-≤) hf b .fst)
+
 isConnectedSuspFun : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'}
        (f : X → Y) (n : HLevel)
     → isConnectedFun n f
@@ -519,6 +549,24 @@ isConnectedSuspFun {X = X} {Y = Y} f n con-f =
         ∙ recₕ n (a , refl)
         ∙ transportRefl (cong F (merid a))
 
+isConnectedSusp : ∀ {ℓ} {X : Type ℓ} (n : HLevel)
+  → isConnected n X
+  → isConnected (suc n) (Susp X)
+isConnectedSusp {X = X} n h = isConnectedFun→isConnected (suc n) $
+  isConnectedComp _ (suspFun (λ (x : X) → tt)) (suc n)
+    (isEquiv→isConnected _ (equivIsEquiv (invEquiv Unit≃SuspUnit)) (suc n))
+    (isConnectedSuspFun _ n (isConnected→isConnectedFun n h))
+
+-- See also `sphereConnected` for S₊
+isConnectedSphere : ∀ (n : ℕ) → isConnected n (S (-1+ n))
+isConnectedSphere zero = isConnectedZero (S (-1+ 0))
+isConnectedSphere (suc n) = isConnectedSusp n (isConnectedSphere n)
+
+isConnected-map-× : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (n : HLevel)
+  (f : B → C) → isConnectedFun n f → isConnectedFun n (map-× (idfun A) f)
+isConnected-map-× n f hf z =
+  isConnectedRetractFromIso _ (invIso $ fiber-map-× f (fst z) (snd z)) (hf (snd z))
+
 -- TODO : Reorganise the following proofs.
 
 inrConnected : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (n : HLevel)