# The induction principle of pushouts

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-06-10.

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

Imports
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


## Idea

The induction principle of pushouts asserts that for every dependent cocone of a type family P over a type X equipped with a cocone c there is a section of P corresponding to c. More precisely, it asserts that the map

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


has a section.

The fact that the induction principle of pushouts is logically equivalent to the dependent universal property of pushouts is shown in dependent-universal-property-pushouts.

## Definition

### The induction principle of pushouts

induction-principle-pushout :
{ l1 l2 l3 l4 : Level} (l : 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 (lsuc l ⊔ l1 ⊔ l2 ⊔ l3 ⊔ l4)
induction-principle-pushout l {X = X} f g c =
(P : X → UU l) → section (dependent-cocone-map f g c P)

module _
{ l1 l2 l3 l4 l : 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 l f g c)
( 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)

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)
( pr2 (ind-c P) h)

left-compute-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
left-compute-ind-induction-principle-pushout h =
pr1 (compute-ind-induction-principle-pushout h)

right-compute-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
right-compute-ind-induction-principle-pushout h =
pr1 (pr2 (compute-ind-induction-principle-pushout h))

path-compute-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)
( left-compute-ind-induction-principle-pushout h)
( right-compute-ind-induction-principle-pushout h)
path-compute-ind-induction-principle-pushout h =
pr2 (pr2 (compute-ind-induction-principle-pushout h))