# The induction principle of pushouts

```agda
module synthetic-homotopy-theory.induction-principle-pushouts where
```

<details><summary>Imports</summary>

```agda
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.sections
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-cocones-under-spans
```

</details>

## Idea

The **induction principle of pushouts** asserts that for every
[dependent cocone](synthetic-homotopy-theory.dependent-cocones-under-spans.md)
of a type family `P` over a type `X` equipped with a
[cocone](synthetic-homotopy-theory.cocones-under-spans.md) `c` there is a
section of `P` corresponding to `c`. More precisely, it asserts that the map

```text
  dependent-cocone-map f g c P : ((x : X) → P x) → dependent-cocone f g c P
```

has a [section](foundation.sections.md).

The fact that the induction principle of pushouts is
[logically equivalent](foundation.logical-equivalences.md) to the
[dependent universal property](synthetic-homotopy-theory.dependent-universal-property-pushouts.md)
of pushouts is shown in
[`dependent-universal-property-pushouts`](synthetic-homotopy-theory.dependent-universal-property-pushouts.md).

## Definition

### The induction principle of pushouts

```agda
induction-principle-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) →
  UUω
induction-principle-pushout {X = X} f g c =
  {l : Level} (P : X → UU l) → section (dependent-cocone-map f g c P)

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)
  ( ind-c : induction-principle-pushout f g c)
  {l : Level} ( P : X → UU l)
  where

  ind-induction-principle-pushout : dependent-cocone f g c P → (x : X) → P x
  ind-induction-principle-pushout = pr1 (ind-c P)

  eq-compute-ind-induction-principle-pushout :
    (h : dependent-cocone f g c P) →
    dependent-cocone-map f g c P (ind-induction-principle-pushout h) ＝ h
  eq-compute-ind-induction-principle-pushout = pr2 (ind-c P)

  compute-ind-induction-principle-pushout :
    (h : dependent-cocone f g c P) →
    htpy-dependent-cocone f g c P
      ( dependent-cocone-map f g c P (ind-induction-principle-pushout h))
      ( h)
  compute-ind-induction-principle-pushout h =
    htpy-eq-dependent-cocone f g c P
      ( dependent-cocone-map f g c P (ind-induction-principle-pushout h))
      ( h)
      ( eq-compute-ind-induction-principle-pushout h)

  compute-horizontal-map-ind-induction-principle-pushout :
    ( h : dependent-cocone f g c P) (a : A) →
    ind-induction-principle-pushout h (horizontal-map-cocone f g c a) ＝
    horizontal-map-dependent-cocone f g c P h a
  compute-horizontal-map-ind-induction-principle-pushout h =
    pr1 (compute-ind-induction-principle-pushout h)

  compute-vertical-map-ind-induction-principle-pushout :
    ( h : dependent-cocone f g c P) (b : B) →
    ind-induction-principle-pushout h (vertical-map-cocone f g c b) ＝
    vertical-map-dependent-cocone f g c P h b
  compute-vertical-map-ind-induction-principle-pushout h =
    pr1 (pr2 (compute-ind-induction-principle-pushout h))

  compute-glue-ind-induction-principle-pushout :
    (h : dependent-cocone f g c P) →
    coherence-htpy-dependent-cocone f g c P
      ( dependent-cocone-map f g c P (ind-induction-principle-pushout h))
      ( h)
      ( compute-horizontal-map-ind-induction-principle-pushout h)
      ( compute-vertical-map-ind-induction-principle-pushout h)
  compute-glue-ind-induction-principle-pushout h =
    pr2 (pr2 (compute-ind-induction-principle-pushout h))
```