Rebase infrastructure for pushouts to span diagrams

src/foundation-core/dependent-identifications.lagda.md

@@ -49,7 +49,7 @@ refl-dependent-identification :
 refl-dependent-identification B = refl
 ```
 
-### Iterated dependent identifications
+### Dependent 2-identifications
 
 ```agda
 module _
@@ -65,3 +65,17 @@ module _
   dependent-identification² α {x'} {y'} p' q' =
     dependent-identification (λ t → dependent-identification B t x' y') α p' q'
 ```
+
+### Double dependent identifications
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
+  where
+
+  double-dependent-identification :
+    {x x' : A} (p : x ＝ x') {y : B x} {y' : B x'} →
+    dependent-identification B p y y' → C x y → C x' y' → UU l3
+  double-dependent-identification refl q z z' =
+    dependent-identification (C _) q z z'
+```

src/foundation.lagda.md

@@ -29,6 +29,7 @@ open import foundation.arithmetic-law-product-and-pi-decompositions public
 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.binary-embeddings public
 open import foundation.binary-equivalences public
 open import foundation.binary-equivalences-unordered-pairs-of-types public
@@ -43,6 +44,7 @@ open import foundation.booleans public
 open import foundation.cantor-schroder-bernstein-escardo public
 open import foundation.cantors-diagonal-argument public
 open import foundation.cartesian-morphisms-arrows public
+open import foundation.cartesian-morphisms-span-diagrams public
 open import foundation.cartesian-product-types public
 open import foundation.cartesian-products-set-quotients public
 open import foundation.category-of-families-of-sets public
@@ -126,6 +128,7 @@ open import foundation.discrete-relaxed-sigma-decompositions public
 open import foundation.discrete-sigma-decompositions public
 open import foundation.discrete-types public
 open import foundation.disjunction public
+open import foundation.disjunction-decidable-propositions public
 open import foundation.double-negation public
 open import foundation.double-negation-modality public
 open import foundation.double-powersets public

src/foundation/action-on-identifications-binary-dependent-functions.lagda.md

@@ -0,0 +1,50 @@
+# The action on identifications of binary dependent functions
+
+```agda
+module foundation.action-on-identifications-binary-dependent-functions where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.action-on-identifications-dependent-functions
+open import foundation.universe-levels
+
+open import foundation-core.dependent-identifications
+open import foundation-core.identity-types
+```
+
+</details>
+
+## Idea
+
+Consider a binary dependent function
+
+```text
+  f : (x : A) (y : B x) → C x y.
+```
+
+The {{#concept "action on identifications" Disambiguation="binary dependent functions" Agda=action-on-identifications-binary-dependent-function}} of `f` on an [identification](foundation-core.identity-types.md) `p : x ＝ x'` in `A` and a [dependent identification](foundation-core.dependent-identifications.md) `q : dependent-identification B p y y'` in `B`, is a _double dependent identification_
+
+```text
+  double-dependent-identification C p q (f x y) (f x' y').
+```
+
+This double dependent identification is defined by identification elimination on `p`. In the case `p ≐ refl`, the action on identifications of `f` is defined to be `apd (f x) q`.
+
+## Definitions
+
+### The action of binary dependent functions on identifications
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}
+  (f : (x : A) (y : B x) → C x y)
+  where
+
+  action-identifications-binary-dependent-function :
+    {x x' : A} (p : x ＝ x') {y : B x} {y' : B x'}
+    (q : dependent-identification B p y y') →
+    double-dependent-identification p q (f x y) (f x' y')
+  action-identifications-binary-dependent-function refl q = apd (f _) q
+```

src/foundation/action-on-identifications-binary-functions.lagda.md

@@ -201,3 +201,4 @@ module _
 - [Action of functions on identifications](foundation.action-on-identifications-functions.md)
 - [Action of functions on higher identifications](foundation.action-on-higher-identifications-functions.md).
 - [Action of dependent functions on identifications](foundation.action-on-identifications-dependent-functions.md).
+- [Action of binary dependent functions on identifications](foundation.action-on-identifications-binary-dependent-functions.md)

src/foundation/action-on-identifications-dependent-functions.lagda.md

@@ -25,7 +25,7 @@ type `B x` while `f y` is an element of type `B y`. However, we can
 along `p` to obtain an element of type `B y` that is comparable to the value
 `f y`. In other words, we can consider the type of
 [dependent identifications](foundation-core.dependent-identifications.md) over
-`p` from `f x` to `f y`. The **dependent action on identifications** of `f` on
+`p` from `f x` to `f y`. The {{#concept "action on identifications" Disambiguation="dependent functions"}} of `f` on
 `p` is a dependent identification
 
 ```text
@@ -34,17 +34,20 @@ along `p` to obtain an element of type `B y` that is comparable to the value
 
 ## Definition
 
-### Functorial action of dependent functions on identity types
+### The action of dependent functions on identifications
 
 ```agda
-apd :
-  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x) {x y : A}
-  (p : x ＝ y) → dependent-identification B p (f x) (f y)
-apd f refl = refl
+module _
+  {l1 l2 : Level} {A : UU l1} {B : A → UU l2} (f : (x : A) → B x)
+  where
+
+  apd : {x y : A} (p : x ＝ y) → dependent-identification B p (f x) (f y)
+  apd refl = refl
 ```
 
 ## See also
 
 - [Action of functions on identifications](foundation.action-on-identifications-functions.md)
 - [Action of functions on higher identifications](foundation.action-on-higher-identifications-functions.md).
 - [Action of binary functions on identifications](foundation.action-on-identifications-binary-functions.md).
+- [Action of binary dependent functions on identifications](foundation.action-on-identifications-binary-dependent-functions.md)

src/foundation/action-on-identifications-functions.lagda.md

@@ -109,3 +109,4 @@ ap-const b refl = refl
 - [Action of functions on higher identifications](foundation.action-on-higher-identifications-functions.md).
 - [Action of binary functions on identifications](foundation.action-on-identifications-binary-functions.md).
 - [Action of dependent functions on identifications](foundation.action-on-identifications-dependent-functions.md).
+- [Action of binary dependent functions on identifications](foundation.action-on-identifications-binary-dependent-functions.md)

src/foundation/base-changes-span-diagrams.lagda.md

@@ -0,0 +1,211 @@
+# Base changes of span diagrams
+
+```agda
+module foundation.base-changes-span-diagrams where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+open import foundation.cartesian-morphisms-arrows
+open import foundation.cartesian-morphisms-span-diagrams
+open import foundation.commuting-squares-of-maps
+open import foundation.dependent-pair-types
+open import foundation.morphisms-arrows
+open import foundation.morphisms-span-diagrams
+open import foundation.span-diagrams
+open import foundation.universe-levels
+```
+
+</details>
+
+## Idea
+
+Consider a [span diagram](foundation.span-diagrams.md) `𝒮 := (A <-f- S -g-> B)`.
+A {{#concept "base change" Disambiguation="span diagram"}} of `𝒮` consists of a
+span diagram `𝒯` and a
+[cartesian morphism](foundation.cartesian-morphisms-span-diagrams.md) of span
+diagrams `𝒯 →ₓ 𝒮`.
+
+## Definitions
+
+### Base changes of span diagrams
+
+```agda
+module _
+  {l1 l2 l3 : Level} (l4 l5 l6 : Level) (𝒮 : span-diagram l1 l2 l3)
+  where
+
+  base-change-span-diagram :
+    UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6)
+  base-change-span-diagram =
+    Σ (span-diagram l4 l5 l6) (λ 𝒯 → cartesian-hom-span-diagram 𝒯 𝒮)
+
+module _
+  {l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
+  (f : base-change-span-diagram l4 l5 l6 𝒮)
+  where
+
+  span-diagram-base-change-span-diagram : span-diagram l4 l5 l6
+  span-diagram-base-change-span-diagram = pr1 f
+
+  domain-span-diagram-base-change-span-diagram : UU l4
+  domain-span-diagram-base-change-span-diagram =
+    domain-span-diagram span-diagram-base-change-span-diagram
+
+  codomain-span-diagram-base-change-span-diagram : UU l5
+  codomain-span-diagram-base-change-span-diagram =
+    codomain-span-diagram span-diagram-base-change-span-diagram
+
+  spanning-type-span-diagram-base-change-span-diagram : UU l6
+  spanning-type-span-diagram-base-change-span-diagram =
+    spanning-type-span-diagram span-diagram-base-change-span-diagram
+
+  left-map-span-diagram-base-change-span-diagram :
+    spanning-type-span-diagram-base-change-span-diagram →
+    domain-span-diagram-base-change-span-diagram
+  left-map-span-diagram-base-change-span-diagram =
+    left-map-span-diagram span-diagram-base-change-span-diagram
+
+  right-map-span-diagram-base-change-span-diagram :
+    spanning-type-span-diagram-base-change-span-diagram →
+    codomain-span-diagram-base-change-span-diagram
+  right-map-span-diagram-base-change-span-diagram =
+    right-map-span-diagram span-diagram-base-change-span-diagram
+
+  cartesian-hom-base-change-span-diagram :
+    cartesian-hom-span-diagram span-diagram-base-change-span-diagram 𝒮
+  cartesian-hom-base-change-span-diagram = pr2 f
+
+  hom-cartesian-hom-base-change-span-diagram :
+    hom-span-diagram span-diagram-base-change-span-diagram 𝒮
+  hom-cartesian-hom-base-change-span-diagram =
+    hom-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+
+  map-domain-cartesian-hom-base-change-span-diagram :
+    domain-span-diagram span-diagram-base-change-span-diagram →
+    domain-span-diagram 𝒮
+  map-domain-cartesian-hom-base-change-span-diagram =
+    map-domain-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  map-codomain-cartesian-hom-base-change-span-diagram :
+    codomain-span-diagram span-diagram-base-change-span-diagram →
+    codomain-span-diagram 𝒮
+  map-codomain-cartesian-hom-base-change-span-diagram =
+    map-codomain-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  spanning-map-cartesian-hom-base-change-span-diagram :
+    spanning-type-span-diagram span-diagram-base-change-span-diagram →
+    spanning-type-span-diagram 𝒮
+  spanning-map-cartesian-hom-base-change-span-diagram =
+    spanning-map-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  left-square-cartesian-hom-base-change-span-diagram :
+    coherence-square-maps
+      ( spanning-map-cartesian-hom-base-change-span-diagram)
+      ( left-map-span-diagram span-diagram-base-change-span-diagram)
+      ( left-map-span-diagram 𝒮)
+      ( map-domain-cartesian-hom-base-change-span-diagram)
+  left-square-cartesian-hom-base-change-span-diagram =
+    left-square-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  left-hom-arrow-cartesian-hom-base-change-span-diagram :
+    hom-arrow
+      ( left-map-span-diagram span-diagram-base-change-span-diagram)
+      ( left-map-span-diagram 𝒮)
+  left-hom-arrow-cartesian-hom-base-change-span-diagram =
+    left-hom-arrow-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  right-square-cartesian-hom-base-change-span-diagram :
+    coherence-square-maps
+      ( spanning-map-cartesian-hom-base-change-span-diagram)
+      ( right-map-span-diagram span-diagram-base-change-span-diagram)
+      ( right-map-span-diagram 𝒮)
+      ( map-codomain-cartesian-hom-base-change-span-diagram)
+  right-square-cartesian-hom-base-change-span-diagram =
+    right-square-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  right-hom-arrow-cartesian-hom-base-change-span-diagram :
+    hom-arrow
+      ( right-map-span-diagram span-diagram-base-change-span-diagram)
+      ( right-map-span-diagram 𝒮)
+  right-hom-arrow-cartesian-hom-base-change-span-diagram =
+    right-hom-arrow-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+
+  is-cartesian-cartesian-hom-base-change-span-diagram :
+    is-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+  is-cartesian-cartesian-hom-base-change-span-diagram =
+    is-cartesian-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+
+  is-left-cartesian-cartesian-hom-base-change-span-diagram :
+    is-left-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+  is-left-cartesian-cartesian-hom-base-change-span-diagram =
+    is-left-cartesian-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+
+  left-cartesian-hom-arrow-cartesian-hom-base-change-span-diagram :
+    cartesian-hom-arrow
+      ( left-map-span-diagram span-diagram-base-change-span-diagram)
+      ( left-map-span-diagram 𝒮)
+  left-cartesian-hom-arrow-cartesian-hom-base-change-span-diagram =
+    left-cartesian-hom-arrow-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+
+  is-right-cartesian-cartesian-hom-base-change-span-diagram :
+    is-right-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( hom-cartesian-hom-base-change-span-diagram)
+  is-right-cartesian-cartesian-hom-base-change-span-diagram =
+    is-right-cartesian-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+
+  right-cartesian-hom-arrow-cartesian-hom-base-change-span-diagram :
+    cartesian-hom-arrow
+      ( right-map-span-diagram span-diagram-base-change-span-diagram)
+      ( right-map-span-diagram 𝒮)
+  right-cartesian-hom-arrow-cartesian-hom-base-change-span-diagram =
+    right-cartesian-hom-arrow-cartesian-hom-span-diagram
+      ( span-diagram-base-change-span-diagram)
+      ( 𝒮)
+      ( cartesian-hom-base-change-span-diagram)
+```