Functoriality of morphisms of arrows

src/foundation-core/coherently-invertible-maps.lagda.md

@@ -674,7 +674,7 @@ Now, by pasting these along the common edge `Rgfg`, we obtain
        |             |             |
     Rg |             | Rgfg        | Rg
        ∨             ∨             ∨
-       g <--------- gfg --------> gm
+       g <--------- gfg ---------> g.
              Rg             gS
 ```
 

src/foundation-core/pullbacks.lagda.md

@@ -196,6 +196,14 @@ module _
   is-pullback-standard-pullback = is-equiv-id
 ```
 
+### The identity cone is a pullback
+
+```agda
+is-pullback-id-cone : {l : Level} (A : UU l) → is-pullback id id (id-cone A)
+is-pullback-id-cone A =
+  is-equiv-is-invertible pr1 (λ where (x , .x , refl) → refl) refl-htpy
+```
+
 ### Pullbacks are preserved under homotopies of parallel cones
 
 ```agda
@@ -208,7 +216,7 @@ module _
     {c : cone f g C} {c' : cone f' g' C} (Hc : htpy-parallel-cone Hf Hg c c') →
     gap f g c ~ map-equiv-standard-pullback-htpy Hf Hg ∘ gap f' g' c'
   triangle-is-pullback-htpy {p , q , H} {p' , q' , H'} (Hp , Hq , HH) z =
-    map-extensionality-standard-pullback f g
+    eq-Eq-standard-pullback f g
       ( Hp z)
       ( Hq z)
       ( ( inv (assoc (ap f (Hp z)) (Hf (p' z) ∙ H' z) (inv (Hg (q' z))))) ∙

src/foundation.lagda.md

@@ -30,6 +30,7 @@ open import foundation.automorphisms public
 open import foundation.axiom-of-choice public
 open import foundation.bands public
 open import foundation.base-changes-span-diagrams public
+open import foundation.bicomposition-functions public
 open import foundation.binary-embeddings public
 open import foundation.binary-equivalences public
 open import foundation.binary-equivalences-unordered-pairs-of-types public
@@ -194,6 +195,7 @@ open import foundation.functoriality-dependent-function-types public
 open import foundation.functoriality-dependent-pair-types public
 open import foundation.functoriality-fibers-of-maps public
 open import foundation.functoriality-function-types public
+open import foundation.functoriality-morphisms-arrows public
 open import foundation.functoriality-propositional-truncation public
 open import foundation.functoriality-pullbacks public
 open import foundation.functoriality-sequential-limits public
@@ -207,6 +209,7 @@ open import foundation.higher-homotopies-morphisms-arrows public
 open import foundation.hilberts-epsilon-operators public
 open import foundation.homotopies public
 open import foundation.homotopies-morphisms-arrows public
+open import foundation.homotopies-morphisms-cospan-diagrams public
 open import foundation.homotopy-algebra public
 open import foundation.homotopy-induction public
 open import foundation.homotopy-preorder-of-types public
@@ -328,6 +331,7 @@ open import foundation.propositional-maps public
 open import foundation.propositional-resizing public
 open import foundation.propositional-truncations public
 open import foundation.propositions public
+open import foundation.pullback-cones public
 open import foundation.pullbacks public
 open import foundation.pullbacks-subtypes public
 open import foundation.quasicoherently-idempotent-maps public

src/foundation/bicomposition-functions.lagda.md

@@ -0,0 +1,76 @@
+# Bicomposition of functions
+
+```agda
+module foundation.bicomposition-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
+open import foundation.function-extensionality
+open import foundation.postcomposition-dependent-functions
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies-composition
+
+open import foundation-core.commuting-squares-of-maps
+open import foundation-core.commuting-triangles-of-maps
+open import foundation-core.contractible-maps
+open import foundation-core.contractible-types
+open import foundation-core.equivalences
+open import foundation-core.fibers-of-maps
+open import foundation-core.function-types
+open import foundation-core.functoriality-dependent-function-types
+open import foundation-core.functoriality-dependent-pair-types
+open import foundation-core.homotopies
+open import foundation-core.identity-types
+open import foundation-core.type-theoretic-principle-of-choice
+```
+
+</details>
+
+## Idea
+
+Given functions `f : A → B` and `g : X → Y` the
+{{#concept "bicomposition function" Disambiguation="types" Agda=bicomp}} is the
+map
+
+```text
+  g ∘ - ∘ f : (B → X) → (A → Y)
+```
+
+defined by `λ h x → g (h (f x))`.
+
+## Definitions
+
+### The bicomposition operation on ordinary functions
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} (f : A → B)
+  {X : UU l3} {Y : UU l4} (g : X → Y)
+  where
+
+  bicomp : (B → X) → (A → Y)
+  bicomp h = g ∘ h ∘ f
+```
+
+### Bicomposition preserves homotopies
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level}
+  {A : UU l1} {B : UU l2} {f f' : A → B} (F : f ~ f')
+  {X : UU l3} {Y : UU l4} {g g' : X → Y} (G : g ~ g')
+  where
+
+  htpy-bicomp : bicomp f g ~ bicomp f' g'
+  htpy-bicomp h = eq-htpy (G ·r (h ∘ f) ∙h (g' ∘ h) ·l F)
+```
+
+## See also
+
+- [Composition algebra](foundation.composition-algebra.md)
+- [Pullback-hom](orthogonal-factorization-systems.pullback-hom.md)

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

@@ -34,15 +34,15 @@ that the cube is presented as a lattice
             A'
           / | \
          /  |  \
-        /   |   \
+        ∨   ∨   ∨
        B'   A    C'
        |\ /   \ /|
        | \     / |
-       |/ \   / \|
+       ∨∨ ∨   ∨ ∨∨
        B    D'   C
         \   |   /
          \  |  /
-          \ | /
+          ∨ ∨ ∨
             D
 ```
 

src/foundation/cospan-diagrams.lagda.md

@@ -21,6 +21,8 @@ and `B` and a [cospan](foundation.cospans.md) `A -f-> X <-g- B` between them.
 
 ## Definitions
 
+### Cospan diagrams
+
 ```agda
 cospan-diagram :
   (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
@@ -40,4 +42,30 @@ module _
   cospan-cospan-diagram :
     cospan l3 left-type-cospan-diagram right-type-cospan-diagram
   cospan-cospan-diagram = pr2 (pr2 c)
+
+  cospanning-type-cospan-diagram : UU l3
+  cospanning-type-cospan-diagram = codomain-cospan cospan-cospan-diagram
+
+  left-map-cospan-diagram :
+    left-type-cospan-diagram → cospanning-type-cospan-diagram
+  left-map-cospan-diagram = left-map-cospan cospan-cospan-diagram
+
+  right-map-cospan-diagram :
+    right-type-cospan-diagram → cospanning-type-cospan-diagram
+  right-map-cospan-diagram = right-map-cospan cospan-cospan-diagram
+```
+
+### The identity cospan diagram
+
+```agda
+id-cospan-diagram : {l : Level} → UU l → cospan-diagram l l l
+id-cospan-diagram A = (A , A , id-cospan A)
+```
+
+### The swapping operation on cospan diagrams
+
+```agda
+swap-cospan-diagram :
+  {l1 l2 l3 : Level} → cospan-diagram l1 l2 l3 → cospan-diagram l2 l1 l3
+swap-cospan-diagram (A , B , c) = (B , A , swap-cospan c)
 ```

src/foundation/cospans.lagda.md

@@ -55,8 +55,7 @@ a morphism of cospan diagrams, as input. Examples of this kind include
 cospan :
   {l1 l2 : Level} (l : Level) (A : UU l1) (B : UU l2) →
   UU (l1 ⊔ l2 ⊔ lsuc l)
-cospan l A B =
-  Σ (UU l) (λ X → (A → X) × (B → X))
+cospan l A B = Σ (UU l) (λ X → (A → X) × (B → X))
 
 module _
   {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} (c : cospan l A B)
@@ -72,6 +71,22 @@ module _
   right-map-cospan = pr2 (pr2 c)
 ```
 
+### The identity cospan
+
+```agda
+id-cospan : {l : Level} (A : UU l) → cospan l A A
+id-cospan A = (A , id , id)
+```
+
+### The swapping operation on cospans
+
+```agda
+swap-cospan :
+  {l1 l2 : Level} {l : Level} {A : UU l1} {B : UU l2} →
+  cospan l A B → cospan l B A
+swap-cospan (C , f , g) = (C , g , f)
+```
+
 ## See also
 
 - The formal dual of cospans is [spans](foundation.spans.md).

src/foundation/dependent-products-pullbacks.lagda.md

@@ -101,7 +101,7 @@ module _
     is-section-map-inv-standard-pullback-Π h =
       eq-htpy
         ( λ i →
-          map-extensionality-standard-pullback (f i) (g i) refl refl
+          eq-Eq-standard-pullback (f i) (g i) refl refl
             ( inv
               ( ( right-unit) ∙
                 ( htpy-eq (is-section-eq-htpy (λ i → pr2 (pr2 (h i)))) i))))
@@ -110,7 +110,7 @@ module _
     is-retraction-map-inv-standard-pullback-Π :
       is-retraction (map-standard-pullback-Π) (map-inv-standard-pullback-Π)
     is-retraction-map-inv-standard-pullback-Π (α , β , γ) =
-      map-extensionality-standard-pullback
+      eq-Eq-standard-pullback
         ( map-Π f)
         ( map-Π g)
         ( refl)
@@ -149,7 +149,7 @@ module _
   triangle-map-standard-pullback-Π h =
     eq-htpy
       ( λ i →
-        map-extensionality-standard-pullback
+        eq-Eq-standard-pullback
           ( f i)
           ( g i)
           ( refl)

src/foundation/dependent-sums-pullbacks.lagda.md

@@ -368,10 +368,7 @@ module _
     is-pullback-tot-is-pullback-family Y f g
       ( id-cone I)
       ( c)
-      ( is-pullback-is-equiv-vertical-maps id id
-        ( id-cone I)
-        ( is-equiv-id)
-        ( is-equiv-id))
+      ( is-pullback-id-cone I)
 
   is-pullback-family-id-cone-is-pullback-tot :
     is-pullback (tot f) (tot g) tot-cone →
@@ -380,10 +377,7 @@ module _
     is-pullback-family-is-pullback-tot Y f g
       ( id-cone I)
       ( c)
-      ( is-pullback-is-equiv-vertical-maps id id
-        ( id-cone I)
-        ( is-equiv-id)
-        ( is-equiv-id))
+      ( is-pullback-id-cone I)
 ```
 
 ## Table of files about pullbacks