Hatcher's acyclic type is acyclic (#1003)

src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md

@@ -27,11 +27,15 @@ open import foundation.universe-levels
 
 open import structured-types.pointed-maps
 open import structured-types.pointed-types
+open import structured-types.pointed-universal-property-contractible-types
 
+open import synthetic-homotopy-theory.acyclic-types
 open import synthetic-homotopy-theory.eckmann-hilton-argument
 open import synthetic-homotopy-theory.functoriality-loop-spaces
 open import synthetic-homotopy-theory.loop-spaces
 open import synthetic-homotopy-theory.powers-of-loops
+open import synthetic-homotopy-theory.suspensions-of-pointed-types
+open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types
 ```
 
 </details>
@@ -71,40 +75,48 @@ algebra-Hatcher-Acyclic-Type l =
 ### Morphisms of types equipped with the structure of Hatcher's acyclic type
 
 ```agda
-hom-algebra-Hatcher-Acyclic-Type :
-  {l1 l2 : Level} → algebra-Hatcher-Acyclic-Type l1 →
-  algebra-Hatcher-Acyclic-Type l2 → UU (l1 ⊔ l2)
-hom-algebra-Hatcher-Acyclic-Type
-  (A , a1 , a2 , r1 , r2) (B , b1 , b2 , s1 , s2) =
-  Σ ( A →∗ B)
-    ( λ f →
-      Σ ( map-Ω f a1 ＝ b1)
-        ( λ u →
-          Σ ( map-Ω f a2 ＝ b2)
-            ( λ v →
-              ( coherence-square-identifications
-                ( ap (map-Ω f) r1)
-                ( map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u)
-                ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
-                ( s1)) ×
-              ( coherence-square-identifications
-                ( ap (map-Ω f) r2)
-                ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
-                ( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙
-                  ( ap
-                    ( power-nat-Ω 2 B)
-                    ( ( preserves-mul-map-Ω f) ∙
-                      ( horizontal-concat-Id² u v))))
-                ( s2)))))
+module _
+  {l1 l2 : Level}
+  ((A , a1 , a2 , r1 , r2) : algebra-Hatcher-Acyclic-Type l1)
+  ((B , b1 , b2 , s1 , s2) : algebra-Hatcher-Acyclic-Type l2)
+  where
+
+  is-hom-pointed-map-algebra-Hatcher-Acyclic-Type : (A →∗ B) → UU l2
+  is-hom-pointed-map-algebra-Hatcher-Acyclic-Type f =
+    Σ ( map-Ω f a1 ＝ b1)
+      ( λ u →
+        Σ ( map-Ω f a2 ＝ b2)
+          ( λ v →
+            ( coherence-square-identifications
+              ( ap (map-Ω f) r1)
+              ( map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u)
+              ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
+              ( s1)) ×
+            ( coherence-square-identifications
+              ( ap (map-Ω f) r2)
+              ( map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)
+              ( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙
+                ( ap
+                  ( power-nat-Ω 2 B)
+                  ( ( preserves-mul-map-Ω f) ∙
+                    ( horizontal-concat-Id² u v))))
+              ( s2))))
+
+  hom-algebra-Hatcher-Acyclic-Type : UU (l1 ⊔ l2)
+  hom-algebra-Hatcher-Acyclic-Type =
+    Σ ( A →∗ B) is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
 ```
 
-### The Hatcher acyclic type is the initial Hatcher acyclic algebra
+### Initial Hatcher acyclic algebras
+
+One characterization of Hatcher's acyclic type is through its universal property
+as being the initial Hatcher acyclic algebra.
 
 ```agda
 is-initial-algebra-Hatcher-Acyclic-Type :
-  {l1 : Level} (l : Level)
-  (A : algebra-Hatcher-Acyclic-Type l1) → UU (l1 ⊔ lsuc l)
-is-initial-algebra-Hatcher-Acyclic-Type l A =
+  {l1 : Level} (A : algebra-Hatcher-Acyclic-Type l1) → UUω
+is-initial-algebra-Hatcher-Acyclic-Type A =
+  {l : Level} →
   (B : algebra-Hatcher-Acyclic-Type l) →
   is-contr (hom-algebra-Hatcher-Acyclic-Type A B)
 ```
@@ -230,6 +242,263 @@ module _
         ( is-torsorial-path refl)
 ```
 
+### For a fixed pointed map, the `is-hom-pointed-map-algebra-Hatcher-Acyclic-Type` family is torsorial
+
+In proving this, it is helpful to consider an equivalent formulation of
+`is-hom-pointed-map-algebra-Hatcher-Acyclic-Type` for which
+[torsoriality](foundation.torsorial-type-families.md) is almost immediate.
+
+```agda
+module _
+  {l1 l2 : Level}
+  ((A , a1 , a2 , r1 , r2) : algebra-Hatcher-Acyclic-Type l1)
+  ((B , b1 , b2 , s1 , s2) : algebra-Hatcher-Acyclic-Type l2)
+  where
+
+  is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' : (A →∗ B) → UU l2
+  is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' f =
+    Σ ( map-Ω f a1 ＝ b1)
+      ( λ u →
+        Σ ( map-Ω f a2 ＝ b2)
+          ( λ v →
+            ( Id
+              ( inv (map-power-nat-Ω 5 f a1 ∙ ap (power-nat-Ω 5 B) u) ∙
+                ( ap (map-Ω f) r1 ∙
+                  (map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v)))
+              ( s1)) ×
+            ( Id
+              ( inv (map-power-nat-Ω 3 f a2 ∙ ap (power-nat-Ω 3 B) v) ∙
+                ( ap (map-Ω f) r2 ∙
+                  ( ( map-power-nat-Ω 2 f (a1 ∙ a2)) ∙
+                    ( ap
+                      ( power-nat-Ω 2 B)
+                      ( ( preserves-mul-map-Ω f) ∙
+                        ( horizontal-concat-Id² u v))))))
+              ( s2))))
+
+module _
+  {l1 l2 : Level}
+  ((A , σ) : algebra-Hatcher-Acyclic-Type l1)
+  ((B , τ) : algebra-Hatcher-Acyclic-Type l2)
+  where
+
+  equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type :
+    (f : A →∗ B) →
+    is-hom-pointed-map-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ) f ≃
+    is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f
+  equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type f =
+    equiv-tot
+      ( λ p →
+        equiv-tot
+          ( λ q →
+            equiv-prod
+              ( equiv-left-transpose-eq-concat' _ _ _ ∘e equiv-inv _ _)
+              ( equiv-left-transpose-eq-concat' _ _ _ ∘e equiv-inv _ _)))
+
+module _
+  {l1 l2 : Level}
+  (A : Pointed-Type l1)
+  (B : Pointed-Type l2)
+  (σ@(a1 , a2 , r1 , r2) : structure-Hatcher-Acyclic-Type A)
+  (f : A →∗ B)
+  where
+
+  is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' :
+    is-torsorial
+      ( λ τ →
+        is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' (A , σ) (B , τ) f)
+  is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type' =
+    is-torsorial-Eq-structure
+      ( is-torsorial-path (map-Ω f a1)) ((map-Ω f a1) , refl)
+      ( is-torsorial-Eq-structure
+        ( is-torsorial-path (map-Ω f a2)) ((map-Ω f a2) , refl)
+        ( is-torsorial-Eq-structure
+          ( is-torsorial-path _)
+          ( _ , refl)
+          ( is-torsorial-path _)))
+
+  abstract
+    is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type :
+      is-torsorial
+        ( λ τ →
+          is-hom-pointed-map-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ) f)
+    is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type =
+      is-contr-equiv
+        ( Σ ( structure-Hatcher-Acyclic-Type B)
+            ( λ τ →
+              is-hom-pointed-map-algebra-Hatcher-Acyclic-Type'
+                ( A , σ)
+                ( B , τ)
+                ( f)))
+        ( equiv-tot
+          ( λ τ →
+            equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
+              ( A , σ)
+              ( B , τ)
+              ( f)))
+        ( is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type')
+```
+
+### Characterization of pointed maps out of Hatcher's acyclic type
+
+For the initial Hatcher acyclic algebra `A` and any pointed type `B`, we exhibit
+an equivalence `(A →∗ B) ≃ structure-Hatcher-Acyclic-Type B`.
+
+We first show that for any Hatcher acyclic algebra `A` (so not necessarily the
+initial one) and a pointed type `B`, a pointed map `f : A →∗ B` induces a
+Hatcher acyclic structure on `B`. Moreover, with this induced structure, the map
+`f` becomes a homomorphism of Hatcher acyclic algebras.
+
+```agda
+module _
+    {l1 l2 : Level}
+    (A : Pointed-Type l1)
+    (B : Pointed-Type l2)
+    (σ@(a1 , a2 , r1 , r2) : structure-Hatcher-Acyclic-Type A)
+    where
+
+  map-Ω-structure-Hatcher-Acyclic-Type :
+    (f : A →∗ B) →
+    ( power-nat-Ω 5 B (map-Ω f a1) ＝
+      power-nat-Ω 3 B (map-Ω f a2)) ×
+    ( power-nat-Ω 3 B (map-Ω f a2) ＝
+      power-nat-Ω 2 B (mul-Ω B (map-Ω f a1) (map-Ω f a2)))
+  pr1 (map-Ω-structure-Hatcher-Acyclic-Type f) =
+    inv (map-power-nat-Ω 5 f a1) ∙ (ap (map-Ω f) r1 ∙ map-power-nat-Ω 3 f a2)
+  pr2 (map-Ω-structure-Hatcher-Acyclic-Type f) =
+    inv (map-power-nat-Ω 3 f a2) ∙
+    ( ap (map-Ω f) r2 ∙
+      ( map-power-nat-Ω 2 f (a1 ∙ a2) ∙
+        ap (power-nat-Ω 2 B) (preserves-mul-map-Ω f)))
+
+  structure-Hatcher-Acyclic-Type-pointed-map :
+    (A →∗ B) → structure-Hatcher-Acyclic-Type B
+  pr1 (structure-Hatcher-Acyclic-Type-pointed-map f) = map-Ω f a1
+  pr1 (pr2 (structure-Hatcher-Acyclic-Type-pointed-map f)) = map-Ω f a2
+  (pr2 (pr2 (structure-Hatcher-Acyclic-Type-pointed-map f))) =
+    map-Ω-structure-Hatcher-Acyclic-Type f
+
+  hom-algebra-Hatcher-Acyclic-Type-pointed-map' :
+    (f : A →∗ B) →
+    is-hom-pointed-map-algebra-Hatcher-Acyclic-Type'
+      ( A , σ)
+      ( B , structure-Hatcher-Acyclic-Type-pointed-map f)
+      ( f)
+  pr1 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f) = refl
+  pr1 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f)) = refl
+  pr1 (pr2 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f))) =
+    ap-binary
+      ( λ p q → inv p ∙ (ap (map-Ω f) r1 ∙ q))
+      ( right-unit {p = map-power-nat-Ω 5 f a1})
+      ( right-unit)
+  pr2 (pr2 (pr2 (hom-algebra-Hatcher-Acyclic-Type-pointed-map' f))) =
+    ap-binary
+      ( λ p q →
+        inv p ∙
+        ( ap (map-Ω f) r2 ∙
+          ( map-power-nat-Ω 2 f (a1 ∙ a2) ∙ ap (power-nat-Ω 2 B) q)))
+      ( right-unit {p = map-power-nat-Ω 3 f a2})
+      ( right-unit {p = preserves-mul-map-Ω f})
+
+  hom-algebra-Hatcher-Acyclic-Type-pointed-map :
+    (f : A →∗ B) →
+    is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
+      ( A , σ)
+      ( B , structure-Hatcher-Acyclic-Type-pointed-map f)
+      ( f)
+  hom-algebra-Hatcher-Acyclic-Type-pointed-map f =
+    map-inv-equiv
+      ( equiv-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
+        ( A , σ)
+        ( B , structure-Hatcher-Acyclic-Type-pointed-map f)
+        ( f))
+      ( hom-algebra-Hatcher-Acyclic-Type-pointed-map' f)
+
+  is-equiv-structure-Hatcher-Acyclic-Type-pointed-map :
+    is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
+    is-equiv structure-Hatcher-Acyclic-Type-pointed-map
+  is-equiv-structure-Hatcher-Acyclic-Type-pointed-map i =
+    is-equiv-htpy-equiv
+      ( equivalence-reasoning
+          A →∗ B
+          ≃ Σ ( A →∗ B)
+              ( λ f →
+                Σ ( structure-Hatcher-Acyclic-Type B)
+                  ( λ τ →
+                    is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
+                      ( A , σ)
+                      ( B , τ)
+                      ( f)))
+            by inv-right-unit-law-Σ-is-contr
+              ( λ f →
+                is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type
+                  ( A)
+                  ( B)
+                  ( σ)
+                  ( f))
+          ≃ Σ ( structure-Hatcher-Acyclic-Type B)
+              ( λ τ → hom-algebra-Hatcher-Acyclic-Type (A , σ) (B , τ))
+            by equiv-left-swap-Σ
+          ≃ structure-Hatcher-Acyclic-Type B
+            by equiv-pr1 (λ τ → i (B , τ)))
+      ( λ f →
+        ap
+          ( pr1)
+          ( inv
+            ( contraction
+              ( is-torsorial-is-hom-pointed-map-algebra-Hatcher-Acyclic-Type A B
+                ( σ)
+                ( f))
+              ( structure-Hatcher-Acyclic-Type-pointed-map f ,
+                hom-algebra-Hatcher-Acyclic-Type-pointed-map f))))
+
+  equiv-pointed-map-Hatcher-Acyclic-Type :
+    is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
+    (A →∗ B) ≃ structure-Hatcher-Acyclic-Type B
+  pr1 (equiv-pointed-map-Hatcher-Acyclic-Type i) =
+    structure-Hatcher-Acyclic-Type-pointed-map
+  pr2 (equiv-pointed-map-Hatcher-Acyclic-Type i) =
+    is-equiv-structure-Hatcher-Acyclic-Type-pointed-map i
+```
+
+### Hatcher's acyclic type is acyclic
+
+**Proof:** For the Hatcher acyclic type `A`, and any pointed type `X`, we have
+
+```text
+ (Σ A →∗ X) ≃ (A →∗ Ω X) ≃ structure-Hatcher-Acyclic-Type (Ω X),
+```
+
+where the first equivalence is the
+[suspension-loop space adjunction](synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types.md),
+the second equivalence was just proven above, and the latter type is
+contractible, as shown by `is-contr-structure-Hatcher-Acyclic-Type-Ω`.
+
+Hence, the suspension `Σ A` of `A` satisfies the
+[universal property of contractible types with respect to pointed types and maps](structured-types.pointed-universal-property-contractible-types.md),
+and hence must be contractible.
+
+```agda
+module _
+  {l1 : Level}
+  ((A , σ) : algebra-Hatcher-Acyclic-Type l1)
+  where
+
+  is-acyclic-is-initial-algebra-Hatcher-Acyclic-Type :
+    is-initial-algebra-Hatcher-Acyclic-Type (A , σ) →
+    is-acyclic (type-Pointed-Type A)
+  is-acyclic-is-initial-algebra-Hatcher-Acyclic-Type i =
+    is-contr-universal-property-contr-Pointed-Type
+      ( suspension-Pointed-Type A)
+      ( λ X →
+        is-contr-equiv
+          ( structure-Hatcher-Acyclic-Type (Ω X))
+          ( equiv-comp
+            ( equiv-pointed-map-Hatcher-Acyclic-Type A (Ω X) σ i)
+            ( equiv-transpose-suspension-loop-adjunction A X))
+          ( is-contr-structure-Hatcher-Acyclic-Type-Ω X))
+```
+
 ## See also
 
 ### Table of files related to cyclic types, groups, and rings