Ian Ray, 15th January 2025

Edited by Ian Ray on 16th March 2025 and 19th June 2025.

The pushout is the universal completion of a span

        C --------> B
        |
        |
        |
        v
        A
        
which consists of a pair of maps with homotopy witnessing that the square

        C --------> B
        |           |
        |           |
        |           |
        v           v
        A --------> P

commutes. The pushout also satisfies a universal property, which in the style of
HoTT/UF is stated as an equivalence of a canonical map. For details on pushouts
see section 23 of Introduction to Homotopy Type Theory by Egbert Rijke (HoTTest
summer school version:
https://github.com/martinescardo/HoTTEST-Summer-School/blob/main/HoTT/hott-intro.pdf)
or chapter 6 section 8 of HoTT book (although it is important to note that the
HoTT book utilizes definitional computation rules). In addition to the above
references, this formalization was inspired by the development found in the
agda-unimath library
(https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.pushouts.html).

In the present work pushouts are defined as a higher inductive type (in the form
of a record type). We assume point and path constructors and the (dependent)
universal property. We will derive other important results like induction and
recursion principles along with the corresponding propositional computation
rules.

Of course, due to Kristina Sojakova's dissertation (and the following paper on
the same topic doi: https://doi.org/10.1145/2775051.2676983), it is well known
that for higher inductive types with propositional computation rules the
following are equivalent:

1) dependent homotopy initiality
2) induction principle with propositional computation rules
3) recursion principle with propositional computation rules and uniqueness
   principle
4) non-dependent homotopy initiality

Sojakova uses the term 'homotopy initiality' of 'algebra morphisms' in the more
general setting. The translation from Sojakova's work to the present work is
roughly:
  algebras ---> cocones
  algebra morphisms ---> cocone morphisms
  homotopy intiality of algebra morphisms ---> universality of maps
                                               (that respect cocone structure)

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt

module UF.Pushouts (fe : Fun-Ext) where

open import MLTT.Spartan
open import UF.Base
open import UF.CoconesofSpans fe
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Subsingletons

\end{code}

We will now define the (dependent and non-dependent) universal properties,
induction principle and the corresponding propositional computation rules for
pushouts.

\begin{code}

module _ {A : 𝓀 Μ‡} {B : π“₯ Μ‡} {C : 𝓦 Μ‡}
         (S : 𝓀' Μ‡) (f : C β†’ A) (g : C β†’ B)
         (s@(i , j , G) : cocone f g S) 
          where

 canonical-map-to-cocone : (X : 𝓣 Μ‡)
                         β†’ (S β†’ X)
                         β†’ cocone f g X
 canonical-map-to-cocone X u = (u ∘ i , u ∘ j , ∼-ap-∘ u G)

 Pushout-Universal-Property : (X : 𝓣 Μ‡)
                            β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓀' βŠ” 𝓣 Μ‡
 Pushout-Universal-Property X = is-equiv (canonical-map-to-cocone X) 

 canonical-map-to-dependent-cocone : (P : S β†’ 𝓣 Μ‡)
                                   β†’ ((x : S) β†’ P x)
                                   β†’ dependent-cocone f g S s P
 canonical-map-to-dependent-cocone P d = (d ∘ i , d ∘ j , Ξ» c β†’ apd d (G c))

 Pushout-Dependent-Universal-Property : (P : S β†’ 𝓣 Μ‡)
                                      β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓀' βŠ” 𝓣 Μ‡
 Pushout-Dependent-Universal-Property P =
  is-equiv (canonical-map-to-dependent-cocone P)

 Pushout-Induction-Principle : (P : S β†’ 𝓣 Μ‡)
                             β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓀' βŠ” 𝓣 Μ‡
 Pushout-Induction-Principle P
  = (l : (a : A) β†’ P (i a))
  β†’ (r : (b : B) β†’ P (j b))
  β†’ ((c : C) β†’ transport P (G c) (l (f c)) ＝ r (g c))
  β†’ (x : S) β†’ P x

 Pushout-Computation-Rule₁ : (P : S β†’ 𝓣 Μ‡)
                           β†’ Pushout-Induction-Principle P
                           β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
 Pushout-Computation-Rule₁ P S-ind
  = (l : (a : A) β†’ P (i a))
  β†’ (r : (b : B) β†’ P (j b))
  β†’ (H : (c : C) β†’ transport P (G c) (l (f c)) ＝ r (g c))
  β†’ (a : A)
  β†’ S-ind l r H (i a) ＝ l a

 Pushout-Computation-Ruleβ‚‚ : (P : S β†’ 𝓣 Μ‡)
                           β†’ Pushout-Induction-Principle P
                           β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
 Pushout-Computation-Ruleβ‚‚ P S-ind
  = (l : (a : A) β†’ P (i a))
  β†’ (r : (b : B) β†’ P (j b))
  β†’ (H : (c : C) β†’ transport P (G c) (l (f c)) ＝ r (g c))
  β†’ (b : B)
  β†’ S-ind l r H (j b) ＝ r b

 Pushout-Computation-Rule₃ : (P : S β†’ 𝓣 Μ‡)
                           β†’ (S-ind : Pushout-Induction-Principle P)
                           β†’ Pushout-Computation-Rule₁ P S-ind
                           β†’ Pushout-Computation-Ruleβ‚‚ P S-ind
                           β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
 Pushout-Computation-Rule₃ P S-ind S-comp₁ S-compβ‚‚
  = (l : (a : A) β†’ P (i a))
  β†’ (r : (b : B) β†’ P (j b))
  β†’ (H : (c : C) β†’ transport P (G c) (l (f c)) ＝ r (g c))
  β†’ (c : C)
  β†’ apd (S-ind l r H) (G c) βˆ™ S-compβ‚‚ l r H (g c)
  ＝ ap (transport P (G c)) (S-comp₁ l r H (f c)) βˆ™ H c

\end{code}

The following are logically equivalent (which is an instance of Sojakova's
result):

1) The dependent universal property
2) The induction principle with propositional computation rules
3) The recursion principle with propositional computation rules and the
   uniqueness principle
4) The universal property.

Below we will derive downward from assumption 1).

TODO. Derive upward from 4) to close the loop, as a means to implement the
equivalence known from Sojakova. This is a work in progress.

\begin{code}

record pushout-exists {A : 𝓀 Μ‡} {B : π“₯ Μ‡} {C : 𝓦 Μ‡} (f : C β†’ A) (g : C β†’ B) : 𝓀ω
 where
 field
  pushout : 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
  inll : A β†’ pushout 
  inrr : B β†’ pushout 
  glue : (c : C) β†’ inll (f c) ＝ inrr (g c)
  pushout-dependent-universal-property
   : {P : pushout β†’ 𝓣  Μ‡}
   β†’ Pushout-Dependent-Universal-Property pushout f g (inll , inrr , glue) P

\end{code}

We need to unpack all the information from the dependent universal property
(i.e. we extract the fact that the fiber of the canonical map is contractible).

\begin{code}

 pushout-cocone : cocone f g pushout
 pushout-cocone = (inll , inrr , glue)

 module _ {P : pushout β†’  𝓣' Μ‡}
          (t : dependent-cocone f g pushout pushout-cocone P)
           where

  pushout-fiber-is-singleton
   : is-contr
      (fiber (canonical-map-to-dependent-cocone pushout f g pushout-cocone P) t)
  pushout-fiber-is-singleton 
   = equivs-are-vv-equivs
      (canonical-map-to-dependent-cocone pushout f g pushout-cocone P)
       pushout-dependent-universal-property t

  pushout-fiber-is-singleton'
   : is-contr
      (Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
       dependent-cocone-family f g pushout pushout-cocone P
        (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t)
  pushout-fiber-is-singleton' 
   = equiv-to-singleton'
      (Ξ£-cong (Ξ» - β†’ dependent-cocone-identity-characterization f g pushout
       pushout-cocone P (- ∘ inll , - ∘ inrr ,  Ξ» c β†’ apd - (glue c)) t))
      pushout-fiber-is-singleton

  pushout-fiber-center
   : Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
      dependent-cocone-family f g pushout pushout-cocone P
       (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t
  pushout-fiber-center = center pushout-fiber-is-singleton'

  pushout-fiber-centrality
   : is-central (Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
                 dependent-cocone-family f g pushout pushout-cocone P
                  (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t)
                pushout-fiber-center 
  pushout-fiber-centrality  = centrality pushout-fiber-is-singleton' 

  pushout-unique-map
   : Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
      dependent-cocone-family f g pushout pushout-cocone P
       (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t
   β†’ (x : pushout) β†’ P x
  pushout-unique-map (d , _) = d

  pushout-inll-homotopy
   : (z : Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
           dependent-cocone-family f g pushout pushout-cocone P
            (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t)
   β†’ (pushout-unique-map z) ∘ inll
    ∼ dependent-cocone-vertical-map f g pushout pushout-cocone P t
  pushout-inll-homotopy (u , K , L , M) = K

  pushout-inrr-homotopy
   : (z : Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
           dependent-cocone-family f g pushout pushout-cocone P
            (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t)
   β†’ (pushout-unique-map z) ∘ inrr
    ∼ dependent-cocone-horizontal-map f g pushout pushout-cocone P t
  pushout-inrr-homotopy (u , K , L , M) = L

  pushout-glue-homotopy
   : (z : Ξ£ d κž‰ ((x : pushout) β†’ P x) ,
           dependent-cocone-family f g pushout pushout-cocone P
            (d ∘ inll , d ∘ inrr ,  Ξ» c β†’ apd d (glue c)) t)
   β†’ ∼-trans (Ξ» - β†’ ap (transport P (glue -)) ((pushout-inll-homotopy z ∘ f) -))
      (dependent-cocone-commuting-square f g pushout pushout-cocone P t)
    ∼ ∼-trans (Ξ» - β†’ apd (pushout-unique-map z) (glue -))
       ((pushout-inrr-homotopy z) ∘ g)
  pushout-glue-homotopy (u , K , L , M) = M

\end{code}

Now we can derive the induction and recursion principles along with the
corresponding computation rules, the uniqueness of maps out of the pushout and
the (non-dependent) universal property.

\begin{code}

 module _ {P : pushout β†’ 𝓣 Μ‡} where

  pushout-induction
   : Pushout-Induction-Principle pushout f g (inll , inrr , glue) P
  pushout-induction l r G
   = pushout-unique-map (l , r , G) (pushout-fiber-center (l , r , G))

  pushout-ind-comp-inll
   : Pushout-Computation-Rule₁ pushout f g (inll , inrr , glue) P
      pushout-induction
  pushout-ind-comp-inll l r G
   = pushout-inll-homotopy (l , r , G) (pushout-fiber-center (l , r , G))

  pushout-ind-comp-inrr
   : Pushout-Computation-Ruleβ‚‚ pushout f g (inll , inrr , glue) P
      pushout-induction
  pushout-ind-comp-inrr l r G
   = pushout-inrr-homotopy (l , r , G) (pushout-fiber-center (l , r , G))

  pushout-ind-comp-glue
   : Pushout-Computation-Rule₃ pushout f g (inll , inrr , glue) P
      pushout-induction pushout-ind-comp-inll pushout-ind-comp-inrr
  pushout-ind-comp-glue l r G c
   = pushout-glue-homotopy (l , r , G) (pushout-fiber-center (l , r , G)) c ⁻¹
   
 module _ {D : 𝓣 Μ‡} where

  pushout-recursion : (l : A β†’ D)
                    β†’ (r : B β†’ D)
                    β†’ ((c : C) β†’ l (f c) ＝ r (g c))
                    β†’ pushout β†’ D
  pushout-recursion l r G =
   pushout-induction l r (Ξ» c β†’ (transport-const (glue c) βˆ™ G c))

  pushout-rec-comp-inll : (l : A β†’ D)
                        β†’ (r : B β†’ D)
                        β†’ (G : (c : C) β†’ l (f c) ＝ r (g c))
                        β†’ (a : A)
                        β†’ pushout-recursion l r G (inll a) ＝ l a
  pushout-rec-comp-inll l r G =
   pushout-ind-comp-inll l r (Ξ» c β†’ (transport-const (glue c) βˆ™ G c))

  pushout-rec-comp-inrr : (l : A β†’ D)
                        β†’ (r : B β†’ D)
                        β†’ (G : (c : C) β†’ l (f c) ＝ r (g c))
                        β†’ (b : B)
                        β†’ pushout-recursion l r G (inrr b) ＝ r b
  pushout-rec-comp-inrr l r G =
   pushout-ind-comp-inrr l r (Ξ» c β†’ (transport-const (glue c) βˆ™ G c))

  pushout-rec-comp-glue
   : (l : A β†’ D)
   β†’ (r : B β†’ D)
   β†’ (G : (c : C) β†’ l (f c) ＝ r (g c))
   β†’ (c : C)
   β†’ ap (pushout-recursion l r G) (glue c) βˆ™ pushout-rec-comp-inrr l r G (g c) 
     ＝ pushout-rec-comp-inll l r G (f c) βˆ™ G c
  pushout-rec-comp-glue l r G c =
   ap (pushout-recursion l r G) (glue c) βˆ™ pushout-rec-comp-inrr l r G (g c)
                                                            ＝⟨ III ⟩
   transport-const (glue c) ⁻¹ βˆ™ apd (pushout-recursion l r G) (glue c)
    βˆ™ pushout-rec-comp-inrr l r G (g c)
                                                            ＝⟨ V ⟩
   transport-const (glue c) ⁻¹
    βˆ™ ap (transport (Ξ» - β†’ D) (glue c)) (pushout-rec-comp-inll l r G (f c))
    βˆ™ (transport-const (glue c) βˆ™ G c)
                                                            ＝⟨ VI ⟩
   transport-const (glue c) ⁻¹
    βˆ™ ap (transport (Ξ» - β†’ D) (glue c)) (pushout-rec-comp-inll l r G (f c))
    βˆ™ transport-const (glue c) βˆ™ G c
                                                            ＝⟨ IX ⟩
   pushout-rec-comp-inll l r G (f c) βˆ™ G c                  ∎
    where
     II : ap (pushout-recursion l r G) (glue c)
         ＝ transport-const (glue c) ⁻¹
          βˆ™ apd (pushout-induction l r (Ξ» - β†’ (transport-const (glue -) βˆ™ G -)))
             (glue c)
     II = apd-from-ap (pushout-recursion l r G) (glue c)
     III = ap (_βˆ™ pushout-rec-comp-inrr l r G (g c)) II 
     IV : apd (pushout-recursion l r G) (glue c)
         βˆ™ pushout-rec-comp-inrr l r G (g c)
         ＝ ap (transport (Ξ» - β†’ D) (glue c))
               (pushout-rec-comp-inll l r G (f c))
         βˆ™ (transport-const (glue c) βˆ™ G c)
     IV = pushout-ind-comp-glue l r (Ξ» - β†’ (transport-const (glue -) βˆ™ G -)) c
     V : transport-const (glue c) ⁻¹ βˆ™ apd (pushout-recursion l r G) (glue c)
         βˆ™ pushout-rec-comp-inrr l r G (g c)
        ＝ transport-const (glue c) ⁻¹
         βˆ™ ap (transport (Ξ» - β†’ D) (glue c)) (pushout-rec-comp-inll l r G (f c))
         βˆ™ (transport-const (glue c) βˆ™ G c)
     V = ap-on-left-is-assoc (transport-const (glue c) ⁻¹)
          {apd (pushout-recursion l r G) (glue c)}
          {ap (transport (Ξ» - β†’ D) (glue c))
           (pushout-rec-comp-inll l r G (f c))}
          {pushout-rec-comp-inrr l r G (g c)}
          {(transport-const (glue c) βˆ™ G c)} IV
     VI = βˆ™assoc (transport-const (glue c) ⁻¹
          βˆ™ ap (transport (Ξ» - β†’ D) (glue c))
               (pushout-rec-comp-inll l r G (f c))) (transport-const (glue c))
               (G c) ⁻¹
     VII' : transport-const (glue c) βˆ™ ap id (pushout-rec-comp-inll l r G (f c))
           ＝ ap (transport (Ξ» - β†’ D) (glue c))
                 (pushout-rec-comp-inll l r G (f c))
            βˆ™ transport-const (glue c)
     VII' = homotopies-are-natural (transport (Ξ» - β†’ D) (glue c)) id
            (Ξ» - β†’ transport-const (glue c)) {_} {_}
            {pushout-rec-comp-inll l r G (f c)}
     VII : ap (transport (Ξ» - β†’ D) (glue c)) (pushout-rec-comp-inll l r G (f c))
           βˆ™ transport-const (glue c)
          ＝ transport-const (glue c) βˆ™ pushout-rec-comp-inll l r G (f c)
     VII = transport (Ξ» - β†’ transport-const (glue c) βˆ™ - 
          ＝ ap (transport (Ξ» - β†’ D) (glue c))
                 (pushout-rec-comp-inll l r G (f c))
                   βˆ™ transport-const (glue c))
                 (ap-id-is-id (pushout-rec-comp-inll l r G (f c))) VII' ⁻¹
     VIII : transport-const (glue c) ⁻¹
            βˆ™ ap (transport (Ξ» - β†’ D) (glue c))
                 (pushout-rec-comp-inll l r G (f c))
            βˆ™ transport-const (glue c)
           ＝ pushout-rec-comp-inll l r G (f c)
     VIII = βˆ™assoc (transport-const (glue c) ⁻¹)
             (ap (transport (Ξ» - β†’ D) (glue c))
             (pushout-rec-comp-inll l r G (f c))) (transport-const (glue c))
             βˆ™ ap-left-inverse (transport-const (glue c)) VII 
     IX = ap (_βˆ™ G c) VIII

 module _ {X : 𝓣 Μ‡} where

  pushout-uniqueness : (s s' : pushout β†’ X)
                     β†’ (H : (a : A) β†’ s (inll a) ＝ s' (inll a))
                     β†’ (H' : (b : B) β†’ s (inrr b) ＝ s' (inrr b))
                     β†’ (G : (c : C)
                       β†’ ap s (glue c) βˆ™ H' (g c) ＝ H (f c) βˆ™ ap s' (glue c))
                     β†’ (x : pushout) β†’ s x ＝ s' x
  pushout-uniqueness s s' H H' G =
   pushout-induction H H' I
    where
     I : (c : C)
       β†’ transport (Ξ» - β†’ s - ＝ s' -) (glue c) (H (f c)) ＝ H' (g c)
     I c = transport (Ξ» - β†’ s - ＝ s' -) (glue c) (H (f c)) ＝⟨ II ⟩
           ap s (glue c) ⁻¹ βˆ™ H (f c) βˆ™ ap s' (glue c)      ＝⟨ III ⟩
           H' (g c)                                         ∎
      where
       II = transport-after-ap' (glue c) s s' (H (f c))
       III = ap s (glue c) ⁻¹ βˆ™ H (f c) βˆ™ ap s' (glue c)   ＝⟨ IV ⟩
             ap s (glue c) ⁻¹ βˆ™ (H (f c) βˆ™ ap s' (glue c)) ＝⟨ V ⟩
             H' (g c)                                      ∎
        where
         IV = βˆ™assoc (ap s (glue c) ⁻¹) (H (f c)) (ap s' (glue c))
         V = ap-left-inverse (ap s (glue c)) (G c ⁻¹)
   
  pushout-universal-property
   : Pushout-Universal-Property pushout f g (inll , inrr , glue) X
  pushout-universal-property = ((ψ , Ο•-ψ) , (ψ , ψ-Ο•))
   where
    Ο• : (pushout β†’ X) β†’ cocone f g X
    Ο• u = canonical-map-to-cocone pushout f g (inll , inrr , glue) X u
    ψ : cocone f g X β†’ (pushout β†’ X)
    ψ (l , r , G) = pushout-recursion l r G
    ψ-Ο• : ψ ∘ Ο• ∼ id
    ψ-Ο• u = dfunext fe (pushout-uniqueness ((ψ ∘ Ο•) u) u
             (pushout-rec-comp-inll (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
             (pushout-rec-comp-inrr (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue))
             (pushout-rec-comp-glue (u ∘ inll) (u ∘ inrr) (∼-ap-∘ u glue)))
    Ο•-ψ : Ο• ∘ ψ ∼ id
    Ο•-ψ (l , r , G) =
     inverse-cocone-map f g X ((Ο• ∘ ψ) (l , r , G)) (l , r , G)
      (pushout-rec-comp-inll l r G , pushout-rec-comp-inrr l r G ,
      ∼-sym (pushout-rec-comp-glue l r G))
   
\end{code}

We now provide a record that asserts the existence of pushouts of arbitrary
spans.

\begin{code}

record pushouts-exist : 𝓀ω
 where
 field
  push-ex : {A : 𝓀 Μ‡} {B : π“₯ Μ‡} {C : 𝓦 Μ‡} (f : C β†’ A) (g : C β†’ B)
          β†’ pushout-exists f g

\end{code}