Retracts of sequential diagrams induce retracts of sequential colimits

src/foundation/retracts-of-maps.lagda.md

@@ -139,7 +139,7 @@ module _
     coherence-htpy-hom-arrow f f (comp-hom-arrow f g f r i) id-hom-arrow
 ```
 
-### The binary relation `g f ↦ g retract-of-map f` asserting that `g` is a retract of the map `f`
+### The binary relation `f g ↦ f retract-of-map g` asserting that `f` is a retract of the map `g`
 
 ```agda
 module _

src/synthetic-homotopy-theory.lagda.md

@@ -77,6 +77,7 @@ open import synthetic-homotopy-theory.pullback-property-pushouts public
 open import synthetic-homotopy-theory.pushout-products public
 open import synthetic-homotopy-theory.pushouts public
 open import synthetic-homotopy-theory.pushouts-of-pointed-types public
+open import synthetic-homotopy-theory.retracts-of-sequential-diagrams public
 open import synthetic-homotopy-theory.sections-descent-circle public
 open import synthetic-homotopy-theory.sequential-colimits public
 open import synthetic-homotopy-theory.sequential-diagrams public

src/synthetic-homotopy-theory/functoriality-sequential-colimits.lagda.md

@@ -19,12 +19,15 @@ open import foundation.function-extensionality
 open import foundation.function-types
 open import foundation.functoriality-dependent-pair-types
 open import foundation.homotopies
+open import foundation.retractions
+open import foundation.retracts-of-types
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies
 
 open import synthetic-homotopy-theory.cocones-under-sequential-diagrams
 open import synthetic-homotopy-theory.equivalences-sequential-diagrams
 open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.retracts-of-sequential-diagrams
 open import synthetic-homotopy-theory.sequential-colimits
 open import synthetic-homotopy-theory.sequential-diagrams
 open import synthetic-homotopy-theory.universal-property-sequential-colimits
@@ -374,7 +377,7 @@ module _
       htpy-preserves-comp-map-hom-standard-sequential-colimit
 ```
 
-### An equivalence of sequential diagrams induces an equivalence of cocones
+### An equivalence of sequential diagrams induces an equivalence of colimits
 
 Additionally, the underlying map of the inverse equivalence is definitionally
 equal to the map induced by the inverse of the equivalence of sequential
@@ -441,6 +444,61 @@ module _
     is-equiv-map-hom-standard-sequential-colimit
 ```
 
+### A retract of sequential diagrams induces a retract of colimits
+
+Additionally, the underlying map of the retraction is definitionally equal to
+the map induced by the retraction of sequential diagrams.
+
+```agda
+module _
+  { l1 l2 : Level} {A : sequential-diagram l1} {B : sequential-diagram l2}
+  ( R : A retract-of-sequential-diagram B)
+  where
+
+  map-inclusion-retract-standard-sequential-colimit :
+    standard-sequential-colimit A → standard-sequential-colimit B
+  map-inclusion-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit B
+      ( inclusion-retract-sequential-diagram A B R)
+
+  map-hom-retraction-retract-standard-sequential-colimit :
+    standard-sequential-colimit B → standard-sequential-colimit A
+  map-hom-retraction-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit A
+      ( hom-retraction-retract-sequential-diagram A B R)
+
+  abstract
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit :
+      is-retraction
+        ( map-inclusion-retract-standard-sequential-colimit)
+        ( map-hom-retraction-retract-standard-sequential-colimit)
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit =
+      ( inv-htpy
+        ( preserves-comp-map-hom-standard-sequential-colimit
+          ( hom-retraction-retract-sequential-diagram A B R)
+          ( inclusion-retract-sequential-diagram A B R))) ∙h
+      ( htpy-map-hom-standard-sequential-colimit-htpy-hom-sequential-diagram
+        ( is-retraction-hom-retraction-retract-sequential-diagram A B R)) ∙h
+      ( preserves-id-map-hom-standard-sequential-colimit)
+
+  retraction-retract-standard-sequential-colimit :
+    retraction
+      ( map-hom-standard-sequential-colimit B
+        ( inclusion-retract-sequential-diagram A B R))
+  pr1 retraction-retract-standard-sequential-colimit =
+    map-hom-retraction-retract-standard-sequential-colimit
+  pr2 retraction-retract-standard-sequential-colimit =
+    is-retraction-map-hom-retraction-retract-standard-sequential-colimit
+
+  retract-retract-standard-sequential-colimit :
+    (standard-sequential-colimit A) retract-of (standard-sequential-colimit B)
+  pr1 retract-retract-standard-sequential-colimit =
+    map-hom-standard-sequential-colimit B
+      ( inclusion-retract-sequential-diagram A B R)
+  pr2 retract-retract-standard-sequential-colimit =
+    retraction-retract-standard-sequential-colimit
+```
+
 ## References
 
 1. Kristina Sojakova, Floris van Doorn, and Egbert Rijke. 2020. Sequential

src/synthetic-homotopy-theory/morphisms-sequential-diagrams.lagda.md

@@ -174,13 +174,13 @@ module _
   ( f g : hom-sequential-diagram A B)
   where
 
-  coherence-htpy-sequential-diagram :
+  coherence-htpy-hom-sequential-diagram :
     ( H :
       ( n : ℕ) →
       ( map-hom-sequential-diagram B f n) ~
       ( map-hom-sequential-diagram B g n)) →
     UU (l1 ⊔ l2)
-  coherence-htpy-sequential-diagram H =
+  coherence-htpy-hom-sequential-diagram H =
     ( n : ℕ) →
     coherence-square-homotopies
       ( map-sequential-diagram B n ·l H n)
@@ -193,7 +193,7 @@ module _
     Σ ( ( n : ℕ) →
         ( map-hom-sequential-diagram B f n) ~
         ( map-hom-sequential-diagram B g n))
-      ( coherence-htpy-sequential-diagram)
+      ( coherence-htpy-hom-sequential-diagram)
 ```
 
 ### Components of homotopies between morphisms of sequential diagrams
@@ -212,7 +212,7 @@ module _
   htpy-htpy-hom-sequential-diagram = pr1 H
 
   coherence-htpy-htpy-hom-sequential-diagram :
-    coherence-htpy-sequential-diagram B f g htpy-htpy-hom-sequential-diagram
+    coherence-htpy-hom-sequential-diagram B f g htpy-htpy-hom-sequential-diagram
   coherence-htpy-htpy-hom-sequential-diagram = pr2 H
 ```
 
@@ -244,7 +244,7 @@ module _
       is-torsorial (htpy-hom-sequential-diagram B f)
     is-torsorial-htpy-sequential-diagram f =
       is-torsorial-Eq-structure
-        ( ev-pair (coherence-htpy-sequential-diagram B f))
+        ( ev-pair (coherence-htpy-hom-sequential-diagram B f))
         ( is-torsorial-binary-htpy (map-hom-sequential-diagram B f))
         ( map-hom-sequential-diagram B f , ev-pair refl-htpy)
         ( is-torsorial-Eq-Π _

src/synthetic-homotopy-theory/retracts-of-sequential-diagrams.lagda.md

@@ -0,0 +1,204 @@
+# Retracts of sequential diagrams
+
+```agda
+module synthetic-homotopy-theory.retracts-of-sequential-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import elementary-number-theory.natural-numbers
+
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.equality-dependent-function-types
+open import foundation.equivalences
+open import foundation.function-types
+open import foundation.homotopies
+open import foundation.homotopy-induction
+open import foundation.identity-types
+open import foundation.retractions
+open import foundation.retracts-of-types
+open import foundation.universe-levels
+
+open import synthetic-homotopy-theory.morphisms-sequential-diagrams
+open import synthetic-homotopy-theory.sequential-diagrams
+```
+
+</details>
+
+## Idea
+
+A {{#concept "retract" Disambiguation="sequential diagram"}} of sequential
+diagrams `A` of `B` is a
+[morphism of sequential diagrams](synthetic-homotopy-theory.morphisms-sequential-diagrams.md)
+`B → A` that is a retraction.
+
+## Definitions
+
+### The predicate of being a retraction of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
+  where
+
+  is-retraction-hom-sequential-diagram : UU l1
+  is-retraction-hom-sequential-diagram =
+    htpy-hom-sequential-diagram A
+      ( comp-hom-sequential-diagram A B A r i)
+      ( id-hom-sequential-diagram A)
+```
+
+### The type of retractions of a morphism of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B)
+  where
+
+  retraction-hom-sequential-diagram : UU (l1 ⊔ l2)
+  retraction-hom-sequential-diagram =
+    Σ (hom-sequential-diagram B A) (is-retraction-hom-sequential-diagram A B i)
+
+  module _
+    (r : retraction-hom-sequential-diagram)
+    where
+
+    hom-retraction-hom-sequential-diagram : hom-sequential-diagram B A
+    hom-retraction-hom-sequential-diagram = pr1 r
+
+    is-retraction-hom-retraction-hom-sequential-diagram :
+      is-retraction-hom-sequential-diagram A B i
+        ( hom-retraction-hom-sequential-diagram)
+    is-retraction-hom-retraction-hom-sequential-diagram = pr2 r
+```
+
+### The predicate that a sequential diagram `A` is a retract of a sequential diagram `B`
+
+```agda
+retract-sequential-diagram :
+  {l1 l2 : Level} (B : sequential-diagram l2) (A : sequential-diagram l1) →
+  UU (l1 ⊔ l2)
+retract-sequential-diagram B A =
+  Σ (hom-sequential-diagram A B) (retraction-hom-sequential-diagram A B)
+```
+
+### The higher coherence in the definition of retracts of sequential diagrams
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (i : hom-sequential-diagram A B) (r : hom-sequential-diagram B A)
+  where
+
+  coherence-retract-sequential-diagram :
+    ( (n : ℕ) →
+      is-retraction
+        ( map-hom-sequential-diagram B i n)
+        ( map-hom-sequential-diagram A r n)) →
+    UU l1
+  coherence-retract-sequential-diagram =
+    coherence-htpy-hom-sequential-diagram A
+      ( comp-hom-sequential-diagram A B A r i)
+      ( id-hom-sequential-diagram A)
+```
+
+### The binary relation `A B ↦ A retract-of-sequential-diagram B` asserting that `A` is a retract of the sequential diagram `B`
+
+```agda
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  where
+
+  infix 6 _retract-of-sequential-diagram_
+
+  _retract-of-sequential-diagram_ : UU (l1 ⊔ l2)
+  _retract-of-sequential-diagram_ = retract-sequential-diagram B A
+
+module _
+  {l1 l2 : Level} (A : sequential-diagram l1) (B : sequential-diagram l2)
+  (R : A retract-of-sequential-diagram B)
+  where
+
+  inclusion-retract-sequential-diagram : hom-sequential-diagram A B
+  inclusion-retract-sequential-diagram = pr1 R
+
+  map-inclusion-retract-sequential-diagram :
+    (n : ℕ) → family-sequential-diagram A n → family-sequential-diagram B n
+  map-inclusion-retract-sequential-diagram =
+    map-hom-sequential-diagram B inclusion-retract-sequential-diagram
+
+  naturality-inclusion-retract-sequential-diagram :
+    naturality-hom-sequential-diagram A B
+      ( map-inclusion-retract-sequential-diagram)
+  naturality-inclusion-retract-sequential-diagram =
+    naturality-map-hom-sequential-diagram B
+      ( inclusion-retract-sequential-diagram)
+
+  retraction-retract-sequential-diagram :
+    retraction-hom-sequential-diagram A B inclusion-retract-sequential-diagram
+  retraction-retract-sequential-diagram = pr2 R
+
+  hom-retraction-retract-sequential-diagram : hom-sequential-diagram B A
+  hom-retraction-retract-sequential-diagram =
+    hom-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( retraction-retract-sequential-diagram)
+
+  map-hom-retraction-retract-sequential-diagram :
+    (n : ℕ) → family-sequential-diagram B n → family-sequential-diagram A n
+  map-hom-retraction-retract-sequential-diagram =
+    map-hom-sequential-diagram A hom-retraction-retract-sequential-diagram
+
+  naturality-hom-retraction-retract-sequential-diagram :
+    naturality-hom-sequential-diagram B A
+      ( map-hom-retraction-retract-sequential-diagram)
+  naturality-hom-retraction-retract-sequential-diagram =
+    naturality-map-hom-sequential-diagram A
+      ( hom-retraction-retract-sequential-diagram)
+
+  is-retraction-hom-retraction-retract-sequential-diagram :
+    is-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( hom-retraction-retract-sequential-diagram)
+  is-retraction-hom-retraction-retract-sequential-diagram =
+    is-retraction-hom-retraction-hom-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( retraction-retract-sequential-diagram)
+
+  is-retraction-map-hom-retraction-retract-sequential-diagram :
+    (n : ℕ) →
+    is-retraction
+      ( map-inclusion-retract-sequential-diagram n)
+      ( map-hom-retraction-retract-sequential-diagram n)
+  is-retraction-map-hom-retraction-retract-sequential-diagram =
+    htpy-htpy-hom-sequential-diagram A
+      ( is-retraction-hom-retraction-retract-sequential-diagram)
+
+  retract-family-retract-sequential-diagram :
+    (n : ℕ) →
+    ( family-sequential-diagram A n) retract-of
+    ( family-sequential-diagram B n)
+  pr1 (retract-family-retract-sequential-diagram n) =
+    map-inclusion-retract-sequential-diagram n
+  pr1 (pr2 (retract-family-retract-sequential-diagram n)) =
+    map-hom-retraction-retract-sequential-diagram n
+  pr2 (pr2 (retract-family-retract-sequential-diagram n)) =
+    is-retraction-map-hom-retraction-retract-sequential-diagram n
+
+  coh-retract-sequential-diagram :
+    coherence-retract-sequential-diagram A B
+      ( inclusion-retract-sequential-diagram)
+      ( hom-retraction-retract-sequential-diagram)
+      ( is-retraction-map-hom-retraction-retract-sequential-diagram)
+  coh-retract-sequential-diagram =
+    coherence-htpy-htpy-hom-sequential-diagram A
+      ( is-retraction-hom-retraction-retract-sequential-diagram)
+```
+
+## See also
+
+- [Retracts of maps](foundation.retracts-of-maps.md)