# Dependent pushout-products

Content created by Egbert Rijke.

Created on 2023-11-23.
Last modified on 2024-04-25.

module synthetic-homotopy-theory.dependent-pushout-products where

Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.universal-property-pushouts


## Idea

The dependent pushout-product is a generalization of the pushout-product. Consider a map f : A → B and a family of maps g : (x : X) → B x → Y x. The dependent pushout-product is the cogap map of the commuting square

                       Σ f id
Σ A (B ∘ f) --------> Σ X B
|                  |
Σ id (g ∘ f) |                  | Σ id g
∨                  ∨
Σ A (Y ∘ f) --------> Σ X Y.
Σ f id


The fiber of the dependent pushout product at (x , y) is equivalent to the join of fibers

  fiber f x * fiber (g x) y


A special case is of interest, where Y is the family of contractible types, and B is a family of propositions.

## Definitions

### Dependent pushout-products

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {X : UU l2} {B : X → UU l3} {Y : X → UU l4}
(f : A → X) (g : (x : X) → B x → Y x)
where

domain-dependent-pushout-product : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
domain-dependent-pushout-product =
pushout
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))

cocone-dependent-pushout-product :
cocone
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( Σ X Y)
pr1 cocone-dependent-pushout-product = map-Σ Y f (λ a → id)
pr1 (pr2 cocone-dependent-pushout-product) = map-Σ Y id g
pr2 (pr2 cocone-dependent-pushout-product) = refl-htpy

abstract
uniqueness-dependent-pushout-product :
is-contr
( Σ ( domain-dependent-pushout-product → Σ X Y)
( λ h →
htpy-cocone
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( cocone-map
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( cocone-pushout
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id)))
( h))
( cocone-dependent-pushout-product)))
uniqueness-dependent-pushout-product =
uniqueness-map-universal-property-pushout
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( cocone-pushout (map-Σ (Y ∘ f) id (g ∘ f)) (map-Σ B f (λ a → id)))
( up-pushout (map-Σ (Y ∘ f) id (g ∘ f)) (map-Σ B f (λ a → id)))
( cocone-dependent-pushout-product)

abstract
dependent-pushout-product : domain-dependent-pushout-product → Σ X Y
dependent-pushout-product =
pr1 (center uniqueness-dependent-pushout-product)

compute-inl-dependent-pushout-product :
( dependent-pushout-product ∘
inl-pushout (map-Σ (Y ∘ f) id (g ∘ f)) (map-Σ B f (λ a → id))) ~
( map-Σ Y f (λ a → id))
compute-inl-dependent-pushout-product =
pr1 (pr2 (center uniqueness-dependent-pushout-product))

compute-inr-dependent-pushout-product :
( dependent-pushout-product ∘
inr-pushout (map-Σ (Y ∘ f) id (g ∘ f)) (map-Σ B f (λ a → id))) ~
map-Σ Y id g
compute-inr-dependent-pushout-product =
pr1 (pr2 (pr2 (center uniqueness-dependent-pushout-product)))

compute-glue-dependent-pushout-product :
statement-coherence-htpy-cocone
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( cocone-map
( map-Σ (Y ∘ f) id (g ∘ f))
( map-Σ B f (λ a → id))
( cocone-pushout (map-Σ (Y ∘ f) id (g ∘ f)) (map-Σ B f (λ a → id)))
( dependent-pushout-product))
( cocone-dependent-pushout-product)
( compute-inl-dependent-pushout-product)
( compute-inr-dependent-pushout-product)
compute-glue-dependent-pushout-product =
pr2 (pr2 (pr2 (center uniqueness-dependent-pushout-product)))