Descent and induction principle of identity types of coequalizers

references.bib

@@ -251,6 +251,19 @@ @online{GGMS24
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
 }
 
+@inproceedings{KvR21,
+  title =        {Path spaces of higher inductive types in homotopy type theory},
+  author =       {Kraus, Nicolai and von Raumer, Jakob},
+  year =         {2021},
+  publisher =    {IEEE Press},
+  abstract =     {The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.},
+  booktitle =    {Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science},
+  articleno =    {7},
+  numpages =     {13},
+  location =     {Vancouver, Canada},
+  series =       {LICS '19}
+}
+
 @article{KECA17,
   title       = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}},
   author      = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},

src/foundation/commuting-triangles-of-maps.lagda.md

@@ -55,20 +55,26 @@ module _
   (left : A → X) (right : B → X) (e : A ≃ B)
   where
 
+  equiv-coherence-triangle-maps-inv-top' :
+    coherence-triangle-maps left right (map-equiv e) ≃
+    coherence-triangle-maps' right left (map-inv-equiv e)
+  equiv-coherence-triangle-maps-inv-top' =
+    equiv-Π
+      ( λ b → left (map-inv-equiv e b) ＝ right b)
+      ( e)
+      ( λ a →
+        equiv-concat
+          ( ap left (is-retraction-map-inv-equiv e a))
+          ( right (map-equiv e a)))
+
   equiv-coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) ≃
     coherence-triangle-maps right left (map-inv-equiv e)
   equiv-coherence-triangle-maps-inv-top =
     ( equiv-inv-htpy
       ( left ∘ (map-inv-equiv e))
       ( right)) ∘e
-    ( equiv-Π
-      ( λ b → left (map-inv-equiv e b) ＝ right b)
-      ( e)
-      ( λ a →
-        equiv-concat
-          ( ap left (is-retraction-map-inv-equiv e a))
-          ( right (map-equiv e a))))
+    ( equiv-coherence-triangle-maps-inv-top')
 
   coherence-triangle-maps-inv-top :
     coherence-triangle-maps left right (map-equiv e) →

src/foundation/equivalences.lagda.md

@@ -16,6 +16,7 @@ open import foundation.equivalence-extensionality
 open import foundation.function-extensionality
 open import foundation.functoriality-fibers-of-maps
 open import foundation.logical-equivalences
+open import foundation.transport-along-identifications
 open import foundation.transposition-identifications-along-equivalences
 open import foundation.truncated-maps
 open import foundation.universal-property-equivalences
@@ -572,6 +573,19 @@ pr1 (equiv-precomp-equiv e C) = _∘e e
 pr2 (equiv-precomp-equiv e C) = is-equiv-precomp-equiv-equiv e
 ```
 
+### Computing transport in a family of equivalence types
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3)
+  where
+
+  tr-equiv-type :
+    {x y : A} (p : x ＝ y) (e : B x ≃ C x) →
+    tr (λ x → B x ≃ C x) p e ＝ equiv-tr C p ∘e e ∘e equiv-tr B (inv p)
+  tr-equiv-type refl e = eq-htpy-equiv refl-htpy
+```
+
 ### A cospan in which one of the legs is an equivalence is a pullback if and only if the corresponding map on the cone is an equivalence
 
 ```agda

src/synthetic-homotopy-theory.lagda.md

@@ -48,15 +48,21 @@ open import synthetic-homotopy-theory.descent-circle-dependent-pair-types public
 open import synthetic-homotopy-theory.descent-circle-equivalence-types public
 open import synthetic-homotopy-theory.descent-circle-function-types public
 open import synthetic-homotopy-theory.descent-circle-subtypes public
+open import synthetic-homotopy-theory.descent-data-coequalizers public
+open import synthetic-homotopy-theory.descent-data-coequalizers-equivalence-families public
+open import synthetic-homotopy-theory.descent-data-coequalizers-function-families public
 open import synthetic-homotopy-theory.descent-data-sequential-colimits public
+open import synthetic-homotopy-theory.descent-property-coequalizers public
 open import synthetic-homotopy-theory.descent-property-sequential-colimits public
 open import synthetic-homotopy-theory.double-loop-spaces public
 open import synthetic-homotopy-theory.eckmann-hilton-argument public
 open import synthetic-homotopy-theory.equifibered-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-cocones-under-equivalences-sequential-diagrams public
 open import synthetic-homotopy-theory.equivalences-coforks-under-equivalences-double-arrows public
 open import synthetic-homotopy-theory.equivalences-dependent-sequential-diagrams public
+open import synthetic-homotopy-theory.equivalences-descent-data-coequalizers public
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams public
+open import synthetic-homotopy-theory.families-descent-data-coequalizers public
 open import synthetic-homotopy-theory.families-descent-data-sequential-colimits public
 open import synthetic-homotopy-theory.flattening-lemma-coequalizers public
 open import synthetic-homotopy-theory.flattening-lemma-pushouts public
@@ -67,6 +73,7 @@ open import synthetic-homotopy-theory.functoriality-sequential-colimits public
 open import synthetic-homotopy-theory.functoriality-suspensions public
 open import synthetic-homotopy-theory.groups-of-loops-in-1-types public
 open import synthetic-homotopy-theory.hatchers-acyclic-type public
+open import synthetic-homotopy-theory.induction-principle-identity-types-coequalizers public
 open import synthetic-homotopy-theory.induction-principle-pushouts public
 open import synthetic-homotopy-theory.infinite-complex-projective-space public
 open import synthetic-homotopy-theory.infinite-cyclic-types public
@@ -83,6 +90,7 @@ open import synthetic-homotopy-theory.morphisms-cocones-under-morphisms-sequenti
 open import synthetic-homotopy-theory.morphisms-coforks-under-morphisms-double-arrows public
 open import synthetic-homotopy-theory.morphisms-dependent-sequential-diagrams public
 open import synthetic-homotopy-theory.morphisms-descent-data-circle public
+open import synthetic-homotopy-theory.morphisms-descent-data-coequalizers public
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams public
 open import synthetic-homotopy-theory.multiplication-circle public
 open import synthetic-homotopy-theory.null-cocones-under-pointed-span-diagrams public
@@ -98,6 +106,7 @@ open import synthetic-homotopy-theory.recursion-principle-pushouts public
 open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.rewriting-pushouts public
 open import synthetic-homotopy-theory.sections-descent-circle public
+open import synthetic-homotopy-theory.sections-descent-data-coequalizers public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public
 open import synthetic-homotopy-theory.sequentially-compact-types public

src/synthetic-homotopy-theory/coequalizers.lagda.md

@@ -77,11 +77,9 @@ module _
           ( horizontal-map-span-cocone-cofork a))
 
     dup-standard-coequalizer :
-      dependent-universal-property-coequalizer a cofork-standard-coequalizer
+      dependent-universal-property-coequalizer cofork-standard-coequalizer
     dup-standard-coequalizer =
       dependent-universal-property-coequalizer-dependent-universal-property-pushout
-        ( a)
-        ( cofork-standard-coequalizer)
         ( λ P →
           tr
             ( λ c →
@@ -103,9 +101,8 @@ module _
               ( P)))
 
     up-standard-coequalizer :
-      universal-property-coequalizer a cofork-standard-coequalizer
+      universal-property-coequalizer cofork-standard-coequalizer
     up-standard-coequalizer =
-      universal-property-dependent-universal-property-coequalizer a
-        ( cofork-standard-coequalizer)
+      universal-property-dependent-universal-property-coequalizer
         ( dup-standard-coequalizer)
 ```

src/synthetic-homotopy-theory/coforks-cocones-under-sequential-diagrams.lagda.md

@@ -233,10 +233,7 @@ module _
 
   dependent-cofork-dependent-cocone-sequential-diagram :
     dependent-cocone-sequential-diagram c P →
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P)
+    dependent-cofork (cofork-cocone-sequential-diagram c) P
   pr1 (dependent-cofork-dependent-cocone-sequential-diagram d) =
     ind-Σ (map-dependent-cocone-sequential-diagram P d)
   pr2 (dependent-cofork-dependent-cocone-sequential-diagram d) =
@@ -377,9 +374,9 @@ module _
     cofork (double-arrow-sequential-diagram A) X →
     cocone-sequential-diagram A X
   pr1 (cocone-sequential-diagram-cofork e) =
-    ev-pair (map-cofork (double-arrow-sequential-diagram A) e)
+    ev-pair (map-cofork e)
   pr2 (cocone-sequential-diagram-cofork e) =
-    ev-pair (coh-cofork (double-arrow-sequential-diagram A) e)
+    ev-pair (coh-cofork e)
 
   abstract
     is-section-cocone-sequential-diagram-cofork :
@@ -431,15 +428,12 @@ module _
     coherence-triangle-maps
       ( cocone-map-sequential-diagram c {Y = Y})
       ( cocone-sequential-diagram-cofork)
-      ( cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( cofork-map (cofork-cocone-sequential-diagram c))
   triangle-cocone-sequential-diagram-cofork h =
     eq-htpy-cocone-sequential-diagram A
       ( cocone-map-sequential-diagram c h)
       ( cocone-sequential-diagram-cofork
         ( cofork-map
-          ( double-arrow-sequential-diagram A)
           ( cofork-cocone-sequential-diagram c)
           ( h)))
       ( refl-htpy-cocone-sequential-diagram _ _)
@@ -468,37 +462,26 @@ module _
   where
 
   dependent-cocone-sequential-diagram-dependent-cofork :
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P) →
+    dependent-cofork (cofork-cocone-sequential-diagram c) P →
     dependent-cocone-sequential-diagram c P
   pr1 (dependent-cocone-sequential-diagram-dependent-cofork e) =
     ev-pair
-      ( map-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
-        ( e))
+      ( map-dependent-cofork P e)
   pr2 (dependent-cocone-sequential-diagram-dependent-cofork e) =
     ev-pair
-      ( coherence-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
-        ( e))
+      ( coherence-dependent-cofork P e)
 
   abstract
     is-section-dependent-cocone-sequential-diagram-dependent-cofork :
       is-section
         ( dependent-cofork-dependent-cocone-sequential-diagram P)
         ( dependent-cocone-sequential-diagram-dependent-cofork)
     is-section-dependent-cocone-sequential-diagram-dependent-cofork e =
-      eq-htpy-dependent-cofork
-        ( double-arrow-sequential-diagram A)
-        ( P)
+      eq-htpy-dependent-cofork P
         ( dependent-cofork-dependent-cocone-sequential-diagram P
           ( dependent-cocone-sequential-diagram-dependent-cofork e))
         ( e)
-        ( refl-htpy-dependent-cofork _ _ _)
+        ( refl-htpy-dependent-cofork _ _)
 
     is-retraction-dependent-cocone-sequential-diagram-dependent-cofork :
       is-retraction
@@ -520,10 +503,7 @@ module _
       ( is-section-dependent-cocone-sequential-diagram-dependent-cofork)
 
   equiv-dependent-cocone-sequential-diagram-dependent-cofork :
-    dependent-cofork
-      ( double-arrow-sequential-diagram A)
-      ( cofork-cocone-sequential-diagram c)
-      ( P) ≃
+    dependent-cofork (cofork-cocone-sequential-diagram c) P ≃
     dependent-cocone-sequential-diagram c P
   pr1 equiv-dependent-cocone-sequential-diagram-dependent-cofork =
     dependent-cocone-sequential-diagram-dependent-cofork
@@ -540,16 +520,11 @@ module _
     coherence-triangle-maps
       ( dependent-cocone-map-sequential-diagram c P)
       ( dependent-cocone-sequential-diagram-dependent-cofork P)
-      ( dependent-cofork-map
-        ( double-arrow-sequential-diagram A)
-        ( cofork-cocone-sequential-diagram c))
+      ( dependent-cofork-map (cofork-cocone-sequential-diagram c))
   triangle-dependent-cocone-sequential-diagram-dependent-cofork h =
     eq-htpy-dependent-cocone-sequential-diagram P
       ( dependent-cocone-map-sequential-diagram c P h)
       ( dependent-cocone-sequential-diagram-dependent-cofork P
-        ( dependent-cofork-map
-          ( double-arrow-sequential-diagram A)
-          ( cofork-cocone-sequential-diagram c)
-          ( h)))
+        ( dependent-cofork-map (cofork-cocone-sequential-diagram c) h))
       ( refl-htpy-dependent-cocone-sequential-diagram _ _)
 ```