Merge pull request #605 from felixwellen/pushout-hlevel

An n-type preservation property of pushouts

Cubical/Foundations/Equiv/Properties.agda

@@ -180,6 +180,10 @@ isPropIsHAEquiv {f = f} ishaef = goal ishaef where
     (isPropΣ (isContr→isProp (isEquiv→isContrHasSection equivF))
              λ s → isPropΠ λ x → isProp→isSet (isContr→isProp (equivF .equiv-proof (f x))) _ _)
 
+-- loop spaces connected by a path are equivalent
+conjugatePathEquiv : {A : Type ℓ} {a b : A} (p : a ≡ b) → (a ≡ a) ≃ (b ≡ b)
+conjugatePathEquiv p = compEquiv (compPathrEquiv p) (compPathlEquiv (sym p))
+
 -- composition on the right induces an equivalence of path types
 compr≡Equiv : {A : Type ℓ} {a b c : A} (p q : a ≡ b) (r : b ≡ c) → (p ≡ q) ≃ (p ∙ r ≡ q ∙ r)
 compr≡Equiv p q r = congEquiv ((λ s → s ∙ r) , compPathr-isEquiv r)

Cubical/HITs/Pushout/KrausVonRaumer.agda

@@ -12,10 +12,21 @@ module Cubical.HITs.Pushout.KrausVonRaumer where
 open import Cubical.Foundations.Everything
 open import Cubical.Functions.Embedding
 open import Cubical.Data.Sigma
-open import Cubical.HITs.Pushout.Base
+open import Cubical.Data.Nat
+open import Cubical.Data.Sum as ⊎
+open import Cubical.HITs.PropositionalTruncation as Trunc
+open import Cubical.HITs.Pushout.Base as ⊔
+open import Cubical.HITs.Pushout.Properties
 
 private
-  interpolate : ∀ {ℓ} {A : Type ℓ} {x y z : A} (q : y ≡ z)
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+    A : Type ℓ
+    B : Type ℓ'
+    C : Type ℓ''
+
+private
+  interpolate : {x y z : A} (q : y ≡ z)
     → PathP (λ i → x ≡ q i → x ≡ z) (_∙ q) (idfun _)
   interpolate q i p j =
     hcomp
@@ -26,13 +37,13 @@ private
         })
       (p j)
 
-  interpolateCompPath : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) {z : A} (q : y ≡ z)
+  interpolateCompPath : {x y : A} (p : x ≡ y) {z : A} (q : y ≡ z)
    → (λ i → interpolate q i (λ j → compPath-filler p q i j)) ≡ refl
   interpolateCompPath p =
     J (λ z q → (λ i → interpolate q i (λ j → compPath-filler p q i j)) ≡ refl)
       (homotopySymInv (λ p i j → compPath-filler p refl (~ i) j) p)
 
-module ElimL {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+module ElimL
   {f : A → B} {g : A → C} {b₀ : B}
   (P : ∀ b → Path (Pushout f g) (inl b₀) (inl b) → Type ℓ''')
   (Q : ∀ c → Path (Pushout f g) (inl b₀) (inr c) → Type ℓ''')
@@ -70,7 +81,7 @@ module ElimL {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type 
        (interpolateCompPath q (push a) ⁻¹)
        refl)
 
-module ElimR {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
+module ElimR
   {f : A → B} {g : A → C} {c₀ : C}
   (P : ∀ b → Path (Pushout f g) (inr c₀) (inl b) → Type ℓ''')
   (Q : ∀ c → Path (Pushout f g) (inr c₀) (inr c) → Type ℓ''')
@@ -110,28 +121,78 @@ module ElimR {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type 
 
 -- Example application: pushouts preserve embeddings
 
-isEmbeddingInr : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''}
-  {f : A → B} (g : A → C)
-  → isEmbedding f → isEmbedding (inr {f = f} {g = g})
-isEmbeddingInr {f = f} g fEmb c₀ c₁ =
+isEmbeddingInr :
+  (f : A → B) (g : A → C)
+  → isEmbedding f → isEmbedding (⊔.inr {f = f} {g = g})
+isEmbeddingInr f g fEmb c₀ c₁ =
   isoToIsEquiv (iso _ (fst ∘ bwd c₁) (snd ∘ bwd c₁) bwdCong)
   where
-  Q : ∀ c → inr c₀ ≡ inr c → Type _
-  Q _ q = fiber (cong inr) q
+  Q : ∀ c → ⊔.inr c₀ ≡ ⊔.inr c → Type _
+  Q _ q = fiber (cong ⊔.inr) q
 
-  P : ∀ b → inr c₀ ≡ inl b → Type _
-  P b p = Σ[ u ∈ fiber f b ] Q _ (p ∙ cong inl (u .snd ⁻¹) ∙ push (u .fst))
+  P : ∀ b → ⊔.inr c₀ ≡ ⊔.inl b → Type _
+  P b p = Σ[ u ∈ fiber f b ] Q _ (p ∙ cong ⊔.inl (u .snd ⁻¹) ∙ push (u .fst))
 
   module Bwd = ElimR P Q
     (refl , refl)
     (λ a p →
       subst
         (P (f a) p  ≃_)
-        (cong (λ w → fiber (cong inr) (p ∙ w)) (lUnit (push a) ⁻¹))
+        (cong (λ w → fiber (cong ⊔.inr) (p ∙ w)) (lUnit (push a) ⁻¹))
         (Σ-contractFst (inhProp→isContr (a , refl) (isEmbedding→hasPropFibers fEmb (f a)))))
 
-  bwd : ∀ c → (t : inr c₀ ≡ inr c) → fiber (cong inr) t
+  bwd : ∀ c → (t : ⊔.inr c₀ ≡ ⊔.inr c) → fiber (cong ⊔.inr) t
   bwd = Bwd.elimR
 
-  bwdCong : ∀ {c} → (r : c₀ ≡ c) → bwd c (cong inr r) .fst ≡ r
-  bwdCong = J (λ c r → bwd c (cong inr r) .fst ≡ r) (cong fst Bwd.refl-β)
+  bwdCong : ∀ {c} → (r : c₀ ≡ c) → bwd c (cong ⊔.inr r) .fst ≡ r
+  bwdCong = J (λ c r → bwd c (cong ⊔.inr r) .fst ≡ r) (cong fst Bwd.refl-β)
+
+
+-- Further Application: Pushouts of emedding-spans of n-Types are n-Types, for n≥0
+module _ (f : A → B) (g : A → C) where
+  inlrJointlySurjective :
+    (z : Pushout f g) → ∥ Σ[ x ∈ (B ⊎ C) ] (⊎.rec inl inr x) ≡ z ∥
+  inlrJointlySurjective =
+    elimProp _
+             (λ _ → isPropPropTrunc)
+             (λ b → ∣ ⊎.inl b , refl ∣)
+             (λ c → ∣ ⊎.inr c , refl ∣)
+
+  preserveHLevelEmbedding :
+    {n : HLevel}
+    → isEmbedding f
+    → isEmbedding g
+    → isOfHLevel (2 + n) B
+    → isOfHLevel (2 + n) C
+    → isOfHLevel (2 + n) (Pushout f g)
+  preserveHLevelEmbedding {n = n} fEmb gEmb isOfHLB isOfHLC =
+    isOfHLevelΩ→isOfHLevel n ΩHLevelPushout
+    where isEmbInr = isEmbeddingInr f g fEmb
+          isEmbInrSwitched = isEmbeddingInr g f gEmb
+
+          equivΩC :  {x : Pushout f g} (c : C) (p : inr c ≡ x)
+                    → (c ≡ c) ≃ (x ≡ x)
+          equivΩC c p = compEquiv (_ , isEmbInr c c) (conjugatePathEquiv p)
+
+          equivΩB :  {x : Pushout f g} (b : B) (p : inl b ≡ x)
+                    → (b ≡ b) ≃ (x ≡ x)
+          equivΩB b p = compEquiv
+                          (compEquiv (_ , isEmbInrSwitched b b)
+                                     (congEquiv pushoutSwitchEquiv))
+                          (conjugatePathEquiv p)
+
+          ΩHLevelPushout : (x : Pushout f g) → isOfHLevel (suc n) (x ≡ x)
+          ΩHLevelPushout x =
+            Trunc.elim
+              (λ _ → isPropIsOfHLevel {A = (x ≡ x)} (suc n))
+              (λ {(⊎.inl b , p) →
+                    isOfHLevelRespectEquiv
+                      (suc n)
+                      (equivΩB b p)
+                      (isOfHLB b b);
+                  (⊎.inr c , p) →
+                    isOfHLevelRespectEquiv
+                      (suc n)
+                      (equivΩC c p)
+                      (isOfHLC c c)})
+              (inlrJointlySurjective x)

Cubical/HITs/Pushout/Properties.agda

@@ -28,6 +28,39 @@ open import Cubical.Data.Unit
 
 open import Cubical.HITs.Pushout.Base
 
+private
+  variable
+    ℓ ℓ' ℓ'' ℓ''' : Level
+    A : Type ℓ
+    B : Type ℓ'
+    C : Type ℓ''
+
+{-
+  Elimination for propositions
+-}
+elimProp : {f : A → B} {g : A → C}
+  → (P : Pushout f g → Type ℓ''')
+  → ((x : Pushout f g) → isProp (P x))
+  → ((b : B) → P (inl b))
+  → ((c : C) → P (inr c))
+  → (x : Pushout f g) → P x
+elimProp P isPropP PB PC (inl x) = PB x
+elimProp P isPropP PB PC (inr x) = PC x
+elimProp {f = f} {g = g} P isPropP PB PC (push a i) =
+  isOfHLevel→isOfHLevelDep 1 isPropP (PB (f a)) (PC (g a)) (push a) i
+
+
+{-
+  Switching the span does not change the pushout
+-}
+pushoutSwitchEquiv : {f : A → B} {g : A → C}
+  → Pushout f g ≃ Pushout g f
+pushoutSwitchEquiv = isoToEquiv (iso f inv leftInv rightInv)
+  where f = λ {(inr x) → inl x; (inl x) → inr x; (push a i) → push a (~ i)}
+        inv = λ {(inr x) → inl x; (inl x) → inr x; (push a i) → push a (~ i)}
+        leftInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
+        rightInv = λ {(inl x) → refl; (inr x) → refl; (push a i) → refl}
+
 {-
   Definition of pushout diagrams
 -}
@@ -316,7 +349,7 @@ record 3x3-span : Type₁ where
 
 
 
-PushoutToProp : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {f : A → B} {g : A → C}
+PushoutToProp : {f : A → B} {g : A → C}
                 {D : Pushout f g → Type ℓ'''}
               → ((x : Pushout f g) → isProp (D x))
               → ((a : B) → D (inl a))