# The dependent universal property of pushouts

```agda
module synthetic-homotopy-theory.dependent-universal-property-pushouts where
```

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-dependent-functions
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.retractions
open import foundation.standard-pullbacks
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-cocones-under-spans
open import synthetic-homotopy-theory.dependent-pullback-property-pushouts
open import synthetic-homotopy-theory.induction-principle-pushouts
open import synthetic-homotopy-theory.universal-property-pushouts
```

</details>

## Idea

The **dependent universal property of pushouts** asserts that every section of a
type family over a [pushout](synthetic-homotopy-theory.pushouts.md) corresponds
in a canonical way uniquely to a
[dependent cocone](synthetic-homotopy-theory.dependent-cocones-under-spans.md)
over the [cocone structure](synthetic-homotopy-theory.cocones-under-spans.md) on
the pushout.

## Definition

### The dependent universal property of pushouts

```agda
dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  UUω
dependent-universal-property-pushout f g {X} c =
  {l : Level} (P : X → UU l) → is-equiv (dependent-cocone-map f g c P)
```

## Properties

### Sections defined by the dependent universal property are unique up to homotopy

```agda
abstract
  uniqueness-dependent-universal-property-pushout :
    { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4} →
    ( f : S → A) (g : S → B) (c : cocone f g X)
    ( dup-c : dependent-universal-property-pushout f g c) →
    {l : Level} (P : X → UU l) ( h : dependent-cocone f g c P) →
    is-contr
      ( Σ ( (x : X) → P x)
          ( λ k →
            htpy-dependent-cocone f g c P (dependent-cocone-map f g c P k) h))
  uniqueness-dependent-universal-property-pushout f g c dup-c P h =
    is-contr-is-equiv'
      ( fiber (dependent-cocone-map f g c P) h)
      ( tot
        ( λ k →
          htpy-eq-dependent-cocone f g c P (dependent-cocone-map f g c P k) h))
      ( is-equiv-tot-is-fiberwise-equiv
        ( λ k →
          is-equiv-htpy-eq-dependent-cocone f g c P
            ( dependent-cocone-map f g c P k)
            ( h)))
      ( is-contr-map-is-equiv (dup-c P) h)
```

### The induction principle of pushouts is equivalent to the dependent universal property of pushouts

#### The induction principle of pushouts implies the dependent universal property of pushouts

```agda
module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X)
  where

  htpy-eq-dependent-cocone-map :
    induction-principle-pushout f g c →
    { l : Level} {P : X → UU l} (h h' : (x : X) → P x) →
    dependent-cocone-map f g c P h ＝ dependent-cocone-map f g c P h' → h ~ h'
  htpy-eq-dependent-cocone-map ind-c {P = P} h h' p =
    ind-induction-principle-pushout f g c ind-c
      ( λ x → h x ＝ h' x)
      ( ( horizontal-htpy-eq-dependent-cocone f g c P
          ( dependent-cocone-map f g c P h)
          ( dependent-cocone-map f g c P h')
          ( p)) ,
        ( vertical-htpy-eq-dependent-cocone f g c P
          ( dependent-cocone-map f g c P h)
          ( dependent-cocone-map f g c P h')
          ( p)) ,
        ( λ s →
          map-compute-dependent-identification-eq-value h h'
            ( coherence-square-cocone f g c s)
            ( horizontal-htpy-eq-dependent-cocone f g c P
              ( dependent-cocone-map f g c P h)
              ( dependent-cocone-map f g c P h')
              ( p)
              ( f s))
            ( vertical-htpy-eq-dependent-cocone f g c P
              ( dependent-cocone-map f g c P h)
              ( dependent-cocone-map f g c P h')
              ( p)
              ( g s))
            ( coherence-square-htpy-eq-dependent-cocone f g c P
              ( dependent-cocone-map f g c P h)
              ( dependent-cocone-map f g c P h')
              ( p)
              ( s))))

  is-retraction-ind-induction-principle-pushout :
    (H : induction-principle-pushout f g c) →
    {l : Level} (P : X → UU l) →
    is-retraction
      ( dependent-cocone-map f g c P)
      ( ind-induction-principle-pushout f g c H P)
  is-retraction-ind-induction-principle-pushout ind-c P h =
    eq-htpy
      ( htpy-eq-dependent-cocone-map
        ( ind-c)
        ( ind-induction-principle-pushout f g c
          ( ind-c)
          ( P)
          ( dependent-cocone-map f g c P h))
        ( h)
        ( eq-compute-ind-induction-principle-pushout f g c ind-c P
          ( dependent-cocone-map f g c P h)))

  dependent-universal-property-pushout-induction-principle-pushout :
    induction-principle-pushout f g c →
    dependent-universal-property-pushout f g c
  dependent-universal-property-pushout-induction-principle-pushout ind-c P =
    is-equiv-is-invertible
      ( ind-induction-principle-pushout f g c ind-c P)
      ( eq-compute-ind-induction-principle-pushout f g c ind-c P)
      ( is-retraction-ind-induction-principle-pushout ind-c P)
```

#### The dependent universal property of pushouts implies the induction principle of pushouts

```agda
induction-principle-pushout-dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  dependent-universal-property-pushout f g c →
  induction-principle-pushout f g c
induction-principle-pushout-dependent-universal-property-pushout
  f g c dup-c P = pr1 (dup-c P)
```

### The dependent pullback property of pushouts is equivalent to the dependent universal property of pushouts

#### The dependent universal property of pushouts implies the dependent pullback property of pushouts

```agda
triangle-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) (P : X → UU l5) →
  let i = pr1 c
      j = pr1 (pr2 c)
      H = pr2 (pr2 c)
  in
  ( dependent-cocone-map f g c P) ~
  ( ( tot (λ h → tot (λ h' → htpy-eq))) ∘
    ( gap
      ( λ (h : (a : A) → P (i a)) → λ s → tr P (H s) (h (f s)))
      ( λ (h : (b : B) → P (j b)) → λ s → h (g s))
      ( cone-dependent-pullback-property-pushout f g c P)))
triangle-dependent-pullback-property-pushout f g (pair i (pair j H)) P h =
  eq-pair-eq-fiber (eq-pair-eq-fiber (inv (is-section-eq-htpy (apd h ∘ H))))

dependent-pullback-property-dependent-universal-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  dependent-universal-property-pushout f g c →
  dependent-pullback-property-pushout f g c
dependent-pullback-property-dependent-universal-property-pushout
  f g (pair i (pair j H)) I P =
  let c = (pair i (pair j H)) in
  is-equiv-top-map-triangle
    ( dependent-cocone-map f g c P)
    ( tot (λ h → tot (λ h' → htpy-eq)))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( _∘ g)
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h →
        is-equiv-tot-is-fiberwise-equiv
          ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
    ( I P)
```

#### The dependent pullback property of pushouts implies the dependent universal property of pushouts

```agda
dependent-universal-property-dependent-pullback-property-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) →
  dependent-pullback-property-pushout f g c →
  dependent-universal-property-pushout f g c
dependent-universal-property-dependent-pullback-property-pushout
  f g (pair i (pair j H)) dpullback-c P =
  let c = (pair i (pair j H)) in
  is-equiv-left-map-triangle
    ( dependent-cocone-map f g c P)
    ( tot (λ h → tot (λ h' → htpy-eq)))
    ( gap
      ( λ h x → tr P (H x) (h (f x)))
      ( _∘ g)
      ( cone-dependent-pullback-property-pushout f g c P))
    ( triangle-dependent-pullback-property-pushout f g c P)
    ( dpullback-c P)
    ( is-equiv-tot-is-fiberwise-equiv
      ( λ h →
        is-equiv-tot-is-fiberwise-equiv
          ( λ h' → funext (λ x → tr P (H x) (h (f x))) (h' ∘ g))))
```

### The nondependent and dependent universal property of pushouts are logically equivalent

This follows from the fact that the
[dependent pullback property of pushouts](synthetic-homotopy-theory.dependent-pullback-property-pushouts.md)
is logically equivalent to the
[pullback property of pushouts](synthetic-homotopy-theory.pullback-property-pushouts.md).

```agda
module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
  (f : S → A) (g : S → B) (c : cocone f g X)
  where

  abstract
    universal-property-dependent-universal-property-pushout :
      dependent-universal-property-pushout f g c →
      universal-property-pushout f g c
    universal-property-dependent-universal-property-pushout dup-c {l} =
      universal-property-pushout-pullback-property-pushout f g c
        ( pullback-property-dependent-pullback-property-pushout f g c
          ( dependent-pullback-property-dependent-universal-property-pushout f g
            ( c)
            ( dup-c)))

    dependent-universal-property-universal-property-pushout :
      universal-property-pushout f g c →
      dependent-universal-property-pushout f g c
    dependent-universal-property-universal-property-pushout up-c =
      dependent-universal-property-dependent-pullback-property-pushout f g c
        ( dependent-pullback-property-pullback-property-pushout f g c
          ( pullback-property-pushout-universal-property-pushout f g c up-c))
```