Closure properties of acyclic maps and types

src/synthetic-homotopy-theory/acyclic-maps.lagda.md

@@ -8,6 +8,8 @@ module synthetic-homotopy-theory.acyclic-maps where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.cartesian-product-types
+open import foundation.cones-over-cospans
 open import foundation.constant-maps
 open import foundation.contractible-maps
 open import foundation.contractible-types
@@ -21,19 +23,30 @@ open import foundation.fibers-of-maps
 open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.functoriality-fibers-of-maps
 open import foundation.homotopies
 open import foundation.identity-types
+open import foundation.inhabited-types
 open import foundation.precomposition-dependent-functions
 open import foundation.precomposition-functions
+open import foundation.propositional-truncations
 open import foundation.propositions
+open import foundation.pullbacks
+open import foundation.torsorial-type-families
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.type-arithmetic-unit-type
 open import foundation.unit-type
+open import foundation.universal-property-cartesian-product-types
 open import foundation.universal-property-dependent-pair-types
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.acyclic-types
+open import synthetic-homotopy-theory.cocones-under-spans
 open import synthetic-homotopy-theory.codiagonals-of-maps
+open import synthetic-homotopy-theory.pushouts
 open import synthetic-homotopy-theory.suspensions-of-types
+open import synthetic-homotopy-theory.universal-property-pushouts
 ```
 
 </details>
@@ -289,6 +302,227 @@ module _
         ( is-epimorphism-is-acyclic-map f af))
 ```
 
+### Acyclic maps are closed under pushouts
+
+We give an outline of the proof before formalizing it.
+
+Suppose we have a pushout square on the left in the diagram
+
+```text
+        g          j
+   S -------> B -------> C
+   |          |          |
+ f |          | j        | id
+   |          |          |
+   v       ⌜  v          v
+   A -------> C -------> C
+        i          id
+```
+
+Then `j` is acyclic if and only if the right square is a pushout, which by
+pushout pasting, is equivalent to the outer rectangle being a pushout. For an
+arbitrary type `X` and `f` acyclic, we note that the following composite
+computes to the identity:
+
+```text
+          cocone-map f (j ∘ g)
+ (C → X) ---------------------> cocone f (j ∘ g) X
+                             ̇= Σ (l : A → X) , Σ (r : C → X) , l ∘ f ~ r ∘ j ∘ g
+     (using the left square)
+                             ≃ Σ (l : A → X) , Σ (r : C → X) , l ∘ f ~ r ∘ i ∘ f
+   (since f is acyclic/epic)
+                             ≃ Σ (l : A → X) , Σ (r : C → X) , l ~ r ∘ i
+                             ≃ Σ (r : C → X) , Σ (l : A → X) , l ~ r ∘ i
+      (contracting at r ∘ i)
+                             ≃ (C → X)
+```
+
+Therefore, `cocone-map f (j ∘ g)` is an equivalence and the outer rectangle is
+indeed a pushout.
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  {C : UU l4} (f : S → A) (g : S → B) (c : cocone f g C)
+  where
+
+  equiv-cocone-postcomp-vertical-map-cocone :
+    is-acyclic-map f →
+    {l5 : Level} (X : UU l5) →
+    cocone f (vertical-map-cocone f g c ∘ g) X ≃ (C → X)
+  equiv-cocone-postcomp-vertical-map-cocone ac X =
+    equivalence-reasoning
+        cocone f (vertical-map-cocone f g c ∘ g) X
+      ≃ cocone f (horizontal-map-cocone f g c ∘ f) X
+        by
+          equiv-tot
+          ( λ u →
+            equiv-tot
+              ( λ v →
+                equiv-concat-htpy'
+                  ( u ∘ f)
+                  ( λ s → ap v (inv-htpy (coherence-square-cocone f g c) s))))
+      ≃ Σ ( A → X)
+          ( λ u →
+            Σ (C → X) (λ v → u ∘ f ＝ v ∘ horizontal-map-cocone f g c ∘ f))
+        by equiv-tot ( λ u → equiv-tot ( λ v → equiv-eq-htpy))
+      ≃ Σ (A → X) (λ u → Σ (C → X) (λ v → u ＝ v ∘ horizontal-map-cocone f g c))
+        by
+          equiv-tot
+          ( λ u →
+            equiv-tot
+              ( λ v →
+                inv-equiv-ap-is-emb (is-epimorphism-is-acyclic-map f ac X)))
+      ≃ Σ (C → X) (λ v → Σ (A → X) (λ u → u ＝ v ∘ horizontal-map-cocone f g c))
+        by
+          equiv-left-swap-Σ
+      ≃ (C → X)
+        by
+          equiv-pr1 (λ v → is-torsorial-path' (v ∘ horizontal-map-cocone f g c))
+
+  is-acyclic-map-vertical-map-cocone-is-pushout :
+    is-pushout f g c →
+    is-acyclic-map f →
+    is-acyclic-map (vertical-map-cocone f g c)
+  is-acyclic-map-vertical-map-cocone-is-pushout po ac =
+    is-acyclic-map-is-epimorphism
+      ( vertical-map-cocone f g c)
+      ( is-epimorphism-universal-property-pushout
+        ( vertical-map-cocone f g c)
+        ( universal-property-pushout-right-universal-property-pushout-rectangle
+            ( f)
+            ( g)
+            ( vertical-map-cocone f g c)
+            ( c)
+            ( cocone-codiagonal-map (vertical-map-cocone f g c))
+            ( universal-property-pushout-is-pushout f g c po)
+            ( λ X →
+              is-equiv-right-factor
+                ( map-equiv (equiv-cocone-postcomp-vertical-map-cocone ac X))
+                ( cocone-map f
+                  ( vertical-map-cocone f g c ∘ g)
+                  ( cocone-comp-horizontal f g
+                    ( vertical-map-cocone f g c)
+                    ( c)
+                    ( cocone-codiagonal-map (vertical-map-cocone f g c))))
+                ( is-equiv-map-equiv
+                  ( equiv-cocone-postcomp-vertical-map-cocone ac X))
+                ( is-equiv-id))))
+
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  {C : UU l4} (f : S → A) (g : S → B) (c : cocone f g C)
+  where
+
+  is-acyclic-map-horizontal-map-cocone-is-pushout :
+    is-pushout f g c →
+    is-acyclic-map g →
+    is-acyclic-map (horizontal-map-cocone f g c)
+  is-acyclic-map-horizontal-map-cocone-is-pushout po =
+    is-acyclic-map-vertical-map-cocone-is-pushout g f
+      ( swap-cocone f g C c)
+      ( is-pushout-swap-cocone-is-pushout f g C c po)
+```
+
+### Acyclic maps are closed under pullbacks
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {X : UU l4} (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  is-acyclic-map-vertical-map-cone-is-pullback :
+    is-pullback f g c →
+    is-acyclic-map g →
+    is-acyclic-map (vertical-map-cone f g c)
+  is-acyclic-map-vertical-map-cone-is-pullback pb ac a =
+    is-acyclic-equiv
+      ( map-fiber-cone f g c a ,
+        is-fiberwise-equiv-map-fiber-cone-is-pullback f g c pb a)
+      ( ac (f a))
+
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
+  {X : UU l4} (f : A → X) (g : B → X) (c : cone f g C)
+  where
+
+  is-acyclic-map-horizontal-map-cone-is-pullback :
+    is-pullback f g c →
+    is-acyclic-map f →
+    is-acyclic-map (horizontal-map-cone f g c)
+  is-acyclic-map-horizontal-map-cone-is-pullback pb =
+    is-acyclic-map-vertical-map-cone-is-pullback g f
+      ( swap-cone f g c)
+      ( is-pullback-swap-cone f g c pb)
+```
+
+### Acyclic types are closed under dependent pair types
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : A → UU l2)
+  where
+
+  is-acyclic-Σ :
+    is-acyclic A → ((a : A) → is-acyclic (B a)) → is-acyclic (Σ A B)
+  is-acyclic-Σ ac-A ac-B =
+    is-acyclic-is-acyclic-map-terminal-map
+      ( Σ A B)
+      ( is-acyclic-map-comp
+        ( terminal-map)
+        ( pr1)
+        ( is-acyclic-map-terminal-map-is-acyclic A ac-A)
+        ( λ a → is-acyclic-equiv (equiv-fiber-pr1 B a) (ac-B a)))
+```
+
+### Acyclic types are closed under binary products
+
+```agda
+module _
+  {l1 l2 : Level} (A : UU l1) (B : UU l2)
+  where
+
+  is-acyclic-prod :
+    is-acyclic A → is-acyclic B → is-acyclic (A × B)
+  is-acyclic-prod ac-A ac-B =
+    is-acyclic-is-acyclic-map-terminal-map
+      ( A × B)
+      ( is-acyclic-map-comp
+        ( terminal-map)
+        ( pr2)
+        ( is-acyclic-map-terminal-map-is-acyclic B ac-B)
+        ( is-acyclic-map-horizontal-map-cone-is-pullback
+          ( terminal-map)
+          ( terminal-map)
+          ( cone-prod A B)
+          ( is-pullback-prod A B)
+          ( is-acyclic-map-terminal-map-is-acyclic A ac-A)))
+```
+
+### Inhabited, locally acyclic types are acyclic
+
+```agda
+module _
+  {l : Level} (A : UU l)
+  where
+
+  is-acyclic-inhabited-is-acyclic-Id :
+    is-inhabited A →
+    ((a b : A) → is-acyclic (a ＝ b)) →
+    is-acyclic A
+  is-acyclic-inhabited-is-acyclic-Id h l-ac =
+    apply-universal-property-trunc-Prop h
+      ( is-acyclic-Prop A)
+      ( λ a →
+        is-acyclic-is-acyclic-map-terminal-map A
+          ( is-acyclic-map-left-factor
+            ( terminal-map)
+            ( point a)
+            ( is-acyclic-map-terminal-map-is-acyclic unit is-acyclic-unit)
+            ( λ b → is-acyclic-equiv (fiber-const a b) (l-ac a b))))
+```
+
 ## See also
 
 - [Dependent epimorphisms](foundation.dependent-epimorphisms.md)

src/synthetic-homotopy-theory/acyclic-types.lagda.md

@@ -11,6 +11,7 @@ open import foundation.contractible-types
 open import foundation.equivalences
 open import foundation.propositions
 open import foundation.retracts-of-types
+open import foundation.unit-type
 open import foundation.universe-levels
 
 open import synthetic-homotopy-theory.functoriality-suspensions
@@ -67,6 +68,16 @@ module _
     is-contr-retract-of (suspension B) (retract-of-suspension-retract-of R) ac
 ```
 
+### Contractible types are acyclic
+
+```agda
+is-acyclic-is-contr : {l : Level} (A : UU l) → is-contr A → is-acyclic A
+is-acyclic-is-contr A = is-contr-suspension-is-contr
+
+is-acyclic-unit : is-acyclic unit
+is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit
+```
+
 ## See also
 
 - [Acyclic maps](synthetic-homotopy-theory.acyclic-maps.md)

src/synthetic-homotopy-theory/cocones-under-spans.lagda.md

@@ -393,3 +393,51 @@ module _
   pr1 (pr2 cocone-hom-arrow) = g
   pr2 (pr2 cocone-hom-arrow) = coh-hom-arrow f g h
 ```
+
+### The swapping function on cocones over spans
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) (X : UU l4)
+  where
+
+  swap-cocone : cocone f g X → cocone g f X
+  pr1 (swap-cocone c) = vertical-map-cocone f g c
+  pr1 (pr2 (swap-cocone c)) = horizontal-map-cocone f g c
+  pr2 (pr2 (swap-cocone c)) = inv-htpy (coherence-square-cocone f g c)
+
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) (X : UU l4)
+  where
+
+  is-involution-swap-cocone : swap-cocone g f X ∘ swap-cocone f g X ~ id
+  is-involution-swap-cocone c =
+    eq-htpy-cocone f g
+      ( swap-cocone g f X (swap-cocone f g X c))
+      ( c)
+      ( ( refl-htpy) ,
+        ( refl-htpy) ,
+        ( λ s →
+          concat
+            ( right-unit)
+            ( coherence-square-cocone f g c s)
+            ( inv-inv (coherence-square-cocone f g c s))))
+
+module _
+  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
+  (f : S → A) (g : S → B) (X : UU l4)
+  where
+
+  is-equiv-swap-cocone : is-equiv (swap-cocone f g X)
+  is-equiv-swap-cocone =
+    is-equiv-is-invertible
+      ( swap-cocone g f X)
+      ( is-involution-swap-cocone g f X)
+      ( is-involution-swap-cocone f g X)
+
+  equiv-swap-cocone : cocone f g X ≃ cocone g f X
+  pr1 equiv-swap-cocone = swap-cocone f g X
+  pr2 equiv-swap-cocone = is-equiv-swap-cocone
+```