# Pushouts

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

<details><summary>Imports</summary>

```agda
open import foundation.action-on-identifications-dependent-functions
open import foundation.action-on-identifications-functions
open import foundation.commuting-squares-of-maps
open import foundation.constant-type-families
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.retractions
open import foundation.sections
open import foundation.transport-along-homotopies
open import foundation.transport-along-identifications
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import reflection.erasing-equality

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

</details>

## Idea

Consider a span `š’®` of types

```text
      f     g
  A <--- S ---> B.
```

A **pushout** of `š’®` is an initial type `X` equipped with a
[cocone structure](synthetic-homotopy-theory.cocones-under-spans.md) of `š’®` in
`X`. In other words, a pushout `X` of `š’®` comes equipped with a cocone structure
`(i , j , H)` where

```text
        g
    S -----> B
    |        |
  f |   H    | j
    āˆØ        āˆØ
    A -----> X,
        i
```

such that for any type `Y`, the following evaluation map is an equivalence

```text
  (X ā†’ Y) ā†’ cocone š’® Y.
```

This condition is the
[universal property of the pushout](synthetic-homotopy-theory.universal-property-pushouts.md)
of `š’®`.

The idea is that the pushout of `š’®` is the universal type that contains the
elements of the types `A` and `B` via the 'inclusions' `i : A ā†’ X` and
`j : B ā†’ X`, and furthermore an identification `i a ļ¼ j b` for every `s : S`
such that `f s ļ¼ a` and `g s ļ¼ b`.

Examples of pushouts include
[suspensions](synthetic-homotopy-theory.suspensions-of-types.md),
[spheres](synthetic-homotopy-theory.spheres.md),
[joins](synthetic-homotopy-theory.joins-of-types.md), and the
[smash product](synthetic-homotopy-theory.smash-products-of-pointed-types.md).

## Postulates

### The standard pushout type

We will assume that for any span

```text
      f     g
  A <--- S ---> B,
```

where `S : UU l1`, `A : UU l2`, and `B : UU l3` there is a pushout in
`UU (l1 āŠ” l2 āŠ” l3)`.

```agda
postulate
  pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S ā†’ A) (g : S ā†’ B) ā†’ UU (l1 āŠ” l2 āŠ” l3)

postulate
  inl-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S ā†’ A) (g : S ā†’ B) ā†’ A ā†’ pushout f g

postulate
  inr-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S ā†’ A) (g : S ā†’ B) ā†’ B ā†’ pushout f g

postulate
  glue-pushout :
    {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
    (f : S ā†’ A) (g : S ā†’ B) ā†’ inl-pushout f g āˆ˜ f ~ inr-pushout f g āˆ˜ g

cocone-pushout :
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B) ā†’ cocone f g (pushout f g)
pr1 (cocone-pushout f g) = inl-pushout f g
pr1 (pr2 (cocone-pushout f g)) = inr-pushout f g
pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g
```

### The dependent cogap map

We postulate the constituents of a section of
`dependent-cocone-map f g (cocone-pushout f g)` up to homotopy of dependent
cocones. This is, assuming
[function extensionality](foundation.function-extensionality.md), precisely the
data of the induction principle of pushouts. We write out each component
separately to accomodate
[optional rewrite rules for the standard pushouts](synthetic-homotopy-theory.rewriting-pushouts.md).

```agda
module _
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B) {P : pushout f g ā†’ UU l4}
  (c : dependent-cocone f g (cocone-pushout f g) P)
  where

  postulate
    dependent-cogap : (x : pushout f g) ā†’ P x

  compute-inl-dependent-cogap :
    (a : A) ā†’
    dependent-cogap (inl-pushout f g a) ļ¼
    horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a
  compute-inl-dependent-cogap a = primEraseEquality compute-inl-dependent-cogap'
    where postulate
      compute-inl-dependent-cogap' :
        dependent-cogap (inl-pushout f g a) ļ¼
        horizontal-map-dependent-cocone f g (cocone-pushout f g) P c a

  compute-inr-dependent-cogap :
    (b : B) ā†’
    dependent-cogap (inr-pushout f g b) ļ¼
    vertical-map-dependent-cocone f g (cocone-pushout f g) P c b
  compute-inr-dependent-cogap b = primEraseEquality compute-inr-dependent-cogap'
    where postulate
      compute-inr-dependent-cogap' :
        dependent-cogap (inr-pushout f g b) ļ¼
        vertical-map-dependent-cocone f g (cocone-pushout f g) P c b

  postulate
    compute-glue-dependent-cogap :
      coherence-htpy-dependent-cocone f g
        ( cocone-pushout f g)
        ( P)
        ( dependent-cocone-map f g (cocone-pushout f g) P dependent-cogap)
        ( c)
        ( compute-inl-dependent-cogap)
        ( compute-inr-dependent-cogap)

  htpy-compute-dependent-cogap :
    htpy-dependent-cocone f g
      ( cocone-pushout f g)
      ( P)
      ( dependent-cocone-map f g (cocone-pushout f g) P dependent-cogap)
      ( c)
  htpy-compute-dependent-cogap =
    ( compute-inl-dependent-cogap ,
      compute-inr-dependent-cogap ,
      compute-glue-dependent-cogap)
```

## Definitions

### The induction principle of standard pushouts

```agda
module _
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B)
  where

  is-section-dependent-cogap :
    {l : Level} {P : pushout f g ā†’ UU l} ā†’
    is-section
      ( dependent-cocone-map f g (cocone-pushout f g) P)
      ( dependent-cogap f g)
  is-section-dependent-cogap {P = P} c =
    eq-htpy-dependent-cocone f g
      ( cocone-pushout f g)
      ( P)
      ( dependent-cocone-map f g (cocone-pushout f g) P (dependent-cogap f g c))
      ( c)
      ( htpy-compute-dependent-cogap f g c)

  induction-principle-pushout' :
    induction-principle-pushout f g (cocone-pushout f g)
  induction-principle-pushout' P =
    ( dependent-cogap f g , is-section-dependent-cogap)

  is-retraction-dependent-cogap :
    {l : Level} {P : pushout f g ā†’ UU l} ā†’
    is-retraction
      ( dependent-cocone-map f g (cocone-pushout f g) P)
      ( dependent-cogap f g)
  is-retraction-dependent-cogap {P = P} =
    is-retraction-ind-induction-principle-pushout f g
      ( cocone-pushout f g)
      ( induction-principle-pushout')
      ( P)
```

### The dependent universal property of standard pushouts

```agda
module _
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B)
  where

  dup-pushout :
    dependent-universal-property-pushout f g (cocone-pushout f g)
  dup-pushout =
    dependent-universal-property-pushout-induction-principle-pushout f g
      ( cocone-pushout f g)
      ( induction-principle-pushout' f g)

  equiv-dup-pushout :
    {l : Level} (P : pushout f g ā†’ UU l) ā†’
    ((x : pushout f g) ā†’ P x) ā‰ƒ dependent-cocone f g (cocone-pushout f g) P
  pr1 (equiv-dup-pushout P) = dependent-cocone-map f g (cocone-pushout f g) P
  pr2 (equiv-dup-pushout P) = dup-pushout P
```

### The cogap map

We define `cogap` and its computation rules in terms of `dependent-cogap` to
ensure the proper computational behaviour when in the presence of strict
computation laws on the point constructors of the standard 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}
  where

  cogap : cocone f g X ā†’ pushout f g ā†’ X
  cogap =
    dependent-cogap f g āˆ˜
    dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g)

  is-section-cogap : is-section (cocone-map f g (cocone-pushout f g)) cogap
  is-section-cogap =
    ( ( triangle-dependent-cocone-map-constant-type-family' f g
        ( cocone-pushout f g)) Ā·r
      ( cogap)) āˆ™h
    ( ( cocone-dependent-cocone-constant-type-family f g
        ( cocone-pushout f g)) Ā·l
      ( is-section-dependent-cogap f g) Ā·r
      ( dependent-cocone-constant-type-family-cocone f g
        ( cocone-pushout f g))) āˆ™h
    ( is-retraction-cocone-dependent-cocone-constant-type-family f g
      ( cocone-pushout f g))

  is-retraction-cogap :
    is-retraction (cocone-map f g (cocone-pushout f g)) cogap
  is-retraction-cogap =
    ( ( cogap) Ā·l
      ( triangle-dependent-cocone-map-constant-type-family' f g
        ( cocone-pushout f g))) āˆ™h
    ( ( dependent-cogap f g) Ā·l
      ( is-section-cocone-dependent-cocone-constant-type-family f g
        ( cocone-pushout f g)) Ā·r
      ( dependent-cocone-map f g (cocone-pushout f g) (Ī» _ ā†’ X))) āˆ™h
    ( is-retraction-dependent-cogap f g)
```

### The universal property of standard pushouts

```agda
up-pushout :
  {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B) ā†’
  universal-property-pushout f g (cocone-pushout f g)
up-pushout f g P =
  is-equiv-is-invertible
    ( cogap f g)
    ( is-section-cogap f g)
    ( is-retraction-cogap f g)

equiv-up-pushout :
  {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
  (f : S ā†’ A) (g : S ā†’ B) (X : UU l4) ā†’ (pushout f g ā†’ X) ā‰ƒ (cocone f g X)
pr1 (equiv-up-pushout f g X) = cocone-map f g (cocone-pushout f g)
pr2 (equiv-up-pushout f g X) = up-pushout f g X
```

### Computation with the cogap map

We define the computation witnesses for the cogap map in terms of the
computation witnesses for the dependent cogap map so that when
[rewriting is enabled for pushouts](synthetic-homotopy-theory.rewriting-pushouts.md),
these witnesses reduce to reflexivities.

```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

  compute-inl-cogap :
    cogap f g c āˆ˜ inl-pushout f g ~ horizontal-map-cocone f g c
  compute-inl-cogap =
    compute-inl-dependent-cogap f g
      ( dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g) c)

  compute-inr-cogap :
    cogap f g c āˆ˜ inr-pushout f g ~ vertical-map-cocone f g c
  compute-inr-cogap =
    compute-inr-dependent-cogap f g
      ( dependent-cocone-constant-type-family-cocone f g (cocone-pushout f g) c)
```

<!-- TODO: find the right infrastructure to make the proof below just an application of a more general construction. Note that this is very almost `coherence-htpy-cocone-coherence-htpy-dependent-cocone-constant-type-family`, but an `apd-constant-type-family` has snuck its way into the proof Issue#1120 -->

```agda
  abstract
    compute-glue-cogap :
      statement-coherence-htpy-cocone f g
        ( cocone-map f g (cocone-pushout f g) (cogap f g c))
        ( c)
        ( compute-inl-cogap)
        ( compute-inr-cogap)
    compute-glue-cogap x =
      is-injective-concat
        ( tr-constant-type-family
          ( glue-pushout f g x)
          ( cogap f g c ((inl-pushout f g āˆ˜ f) x)))
        ( ( inv
            ( assoc
              ( tr-constant-type-family
                ( glue-pushout f g x)
                ( cogap f g c
                  ( horizontal-map-cocone f g (cocone-pushout f g) (f x))))
              ( ap (cogap f g c) (glue-pushout f g x))
              ( compute-inr-cogap (g x)))) āˆ™
          ( ap
            ( _āˆ™ compute-inr-cogap (g x))
            ( inv
              ( apd-constant-type-family (cogap f g c) (glue-pushout f g x)))) āˆ™
          ( compute-glue-dependent-cogap f g
            ( dependent-cocone-constant-type-family-cocone f g
              ( cocone-pushout f g)
              ( c))
            ( x)) āˆ™
          ( inv
            ( assoc
              ( ap
                ( tr (Ī» _ ā†’ X) (glue-pushout f g x))
                ( compute-inl-cogap (f x)))
              ( tr-constant-type-family
                ( glue-pushout f g x)
                ( pr1 c (f x)))
              ( coherence-square-cocone f g c x))) āˆ™
          ( ap
            ( _āˆ™ coherence-square-cocone f g c x)
            ( inv
              ( naturality-tr-constant-type-family
                ( glue-pushout f g x)
                ( compute-inl-cogap (f x))))) āˆ™
            ( assoc
              ( tr-constant-type-family
                ( glue-pushout f g x)
                ( cogap f g c (inl-pushout f g (f x))))
              ( compute-inl-cogap (f x))
              ( coherence-square-cocone f g c x)))

  htpy-compute-cogap :
    htpy-cocone f g
      ( cocone-map f g (cocone-pushout f g) (cogap f g c))
      ( c)
  htpy-compute-cogap =
    ( compute-inl-cogap , compute-inr-cogap , compute-glue-cogap)
```

### The small predicate of being a pushout cocone

```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

  is-pushout : UU (l1 āŠ” l2 āŠ” l3 āŠ” l4)
  is-pushout = is-equiv (cogap f g c)

  is-prop-is-pushout : is-prop is-pushout
  is-prop-is-pushout = is-property-is-equiv (cogap f g c)

  is-pushout-Prop : Prop (l1 āŠ” l2 āŠ” l3 āŠ” l4)
  pr1 is-pushout-Prop = is-pushout
  pr2 is-pushout-Prop = is-prop-is-pushout
```

## Properties

### Pushout cocones satisfy the universal property of the pushout

```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

  universal-property-pushout-is-pushout :
    is-pushout f g c ā†’ universal-property-pushout f g c
  universal-property-pushout-is-pushout po =
    up-pushout-up-pushout-is-equiv f g
      ( cocone-pushout f g)
      ( c)
      ( cogap f g c)
      ( htpy-cocone-map-universal-property-pushout f g
        ( cocone-pushout f g)
        ( up-pushout f g)
        ( c))
      ( po)
      ( up-pushout f g)

  is-pushout-universal-property-pushout :
    universal-property-pushout f g c ā†’ is-pushout f g c
  is-pushout-universal-property-pushout =
    is-equiv-up-pushout-up-pushout f g
      ( cocone-pushout f g)
      ( c)
      ( cogap f g c)
      ( htpy-cocone-map-universal-property-pushout f g
        ( cocone-pushout f g)
        ( up-pushout f g)
        ( c))
      ( up-pushout f g)
```

### Fibers of the cogap map

We characterize the [fibers](foundation-core.fibers-of-maps.md) of the cogap map
as a pushout of fibers. This is an application of the
[flattening lemma for pushouts](synthetic-homotopy-theory.flattening-lemma-pushouts.md).

Given a pushout square with a
[cocone](synthetic-homotopy-theory.cocones-under-spans.md)

```text
       g
   S ----> B
   |       | \
 f |    inr|  \  n
   āˆØ     āŒœ āˆØ   \
   A ----> āˆ™    \
    \ inl   \   |
  m  \  cogap\  |
      \       āˆØ āˆØ
       \-----> X
```

we have, for every `x : X`, a pushout square of fibers:

```text
    fiber (m āˆ˜ f) x ---> fiber (cogap āˆ˜ inr) x
           |                       |
           |                       |
           āˆØ                     āŒœ āˆØ
 fiber (cogap āˆ˜ inl) x ----> fiber cogap x
```

```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) (x : X)
  where

  equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span :
    fiber (horizontal-map-cocone f g c āˆ˜ f) x ā‰ƒ
    fiber (cogap f g c āˆ˜ inl-pushout f g āˆ˜ f) x
  equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span =
    equiv-tot (Ī» s ā†’ equiv-concat (compute-inl-cogap f g c (f s)) x)

  equiv-fiber-horizontal-map-cocone-cogap-inl :
    fiber (horizontal-map-cocone f g c) x ā‰ƒ
    fiber (cogap f g c āˆ˜ inl-pushout f g) x
  equiv-fiber-horizontal-map-cocone-cogap-inl =
    equiv-tot (Ī» a ā†’ equiv-concat (compute-inl-cogap f g c a) x)

  equiv-fiber-vertical-map-cocone-cogap-inr :
    fiber (vertical-map-cocone f g c) x ā‰ƒ
    fiber (cogap f g c āˆ˜ inr-pushout f g) x
  equiv-fiber-vertical-map-cocone-cogap-inr =
    equiv-tot (Ī» b ā†’ equiv-concat (compute-inr-cogap f g c b) x)

  horizontal-map-span-cogap-fiber :
    fiber (horizontal-map-cocone f g c āˆ˜ f) x ā†’
    fiber (horizontal-map-cocone f g c) x
  horizontal-map-span-cogap-fiber =
    map-Ī£-map-base f (Ī» a ā†’ horizontal-map-cocone f g c a ļ¼ x)
```

Since our pushout square of fibers has `fiber (m āˆ˜ f) x` as its top-left corner
and not `fiber (n āˆ˜ g) x`, things are "left-biased". For this reason, the
following map is constructed as a composition which makes a later coherence
square commute (almost) trivially.

```agda
  vertical-map-span-cogap-fiber :
    fiber (horizontal-map-cocone f g c āˆ˜ f) x ā†’
    fiber (vertical-map-cocone f g c) x
  vertical-map-span-cogap-fiber =
    ( map-inv-equiv equiv-fiber-vertical-map-cocone-cogap-inr) āˆ˜
    ( horizontal-map-span-flattening-pushout
      ( Ī» y ā†’ (cogap f g c y) ļ¼ x) f g (cocone-pushout f g)) āˆ˜
    ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span)

  statement-universal-property-pushout-cogap-fiber : UUĻ‰
  statement-universal-property-pushout-cogap-fiber =
    { l : Level} ā†’
    Ī£ ( cocone
        ( horizontal-map-span-cogap-fiber)
        ( vertical-map-span-cogap-fiber)
        ( fiber (cogap f g c) x))
      ( universal-property-pushout-Level l
        ( horizontal-map-span-cogap-fiber)
        ( vertical-map-span-cogap-fiber))

  universal-property-pushout-cogap-fiber :
    statement-universal-property-pushout-cogap-fiber
  universal-property-pushout-cogap-fiber =
    universal-property-pushout-extension-by-equivalences
      ( vertical-map-span-flattening-pushout
        ( Ī» y ā†’ cogap f g c y ļ¼ x)
        ( f)
        ( g)
        ( cocone-pushout f g))
      ( horizontal-map-span-flattening-pushout
        ( Ī» y ā†’ cogap f g c y ļ¼ x)
        ( f)
        ( g)
        ( cocone-pushout f g))
      ( horizontal-map-span-cogap-fiber)
      ( vertical-map-span-cogap-fiber)
      ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl)
      ( map-equiv equiv-fiber-vertical-map-cocone-cogap-inr)
      ( map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span)
      ( cocone-flattening-pushout
        ( Ī» y ā†’ cogap f g c y ļ¼ x)
        ( f)
        ( g)
        ( cocone-pushout f g))
      ( flattening-lemma-pushout
        ( Ī» y ā†’ cogap f g c y ļ¼ x)
        ( f)
        ( g)
        ( cocone-pushout f g)
        ( up-pushout f g))
      ( refl-htpy)
      ( Ī» _ ā†’
        inv
          ( is-section-map-inv-equiv
            ( equiv-fiber-vertical-map-cocone-cogap-inr)
            ( _)))
      ( is-equiv-map-equiv equiv-fiber-horizontal-map-cocone-cogap-inl)
      ( is-equiv-map-equiv equiv-fiber-vertical-map-cocone-cogap-inr)
      ( is-equiv-map-equiv
        ( equiv-fiber-horizontal-map-cocone-cogap-inl-horizontal-span))
```

We record the following auxiliary lemma which says that if we have types `T`,
`F` and `G` such that `T ā‰ƒ fiber (m āˆ˜ f) x`, `F ā‰ƒ fiber (cogap āˆ˜ inl) x` and
`G ā‰ƒ fiber (cogap āˆ˜ inr) x`, together with suitable maps `u : T ā†’ F` and
`v : T ā†’ G`, then we get a pushout square:

```text
          v
   T ----------> G
   |             |
 u |             |
   āˆØ           āŒœ āˆØ
   F ----> fiber cogap x
```

Thus, this lemma is useful in case we have convenient descriptions of the
fibers.

```agda
  module _
    { l5 l6 l7 : Level} (T : UU l5) (F : UU l6) (G : UU l7)
    ( i : F ā‰ƒ fiber (horizontal-map-cocone f g c) x)
    ( j : G ā‰ƒ fiber (vertical-map-cocone f g c) x)
    ( k : T ā‰ƒ fiber (horizontal-map-cocone f g c āˆ˜ f) x)
    ( u : T ā†’ F)
    ( v : T ā†’ G)
    ( coh-l :
      coherence-square-maps
        ( map-equiv k)
        ( u)
        ( horizontal-map-span-cogap-fiber)
        ( map-equiv i))
    ( coh-r :
      coherence-square-maps
        ( v)
        ( map-equiv k)
        ( map-equiv j)
        ( vertical-map-span-cogap-fiber))
    where

    universal-property-pushout-cogap-fiber-up-to-equiv :
      { l : Level} ā†’
      ( Ī£ ( cocone u v (fiber (cogap f g c) x))
          ( Ī» c ā†’ universal-property-pushout-Level l u v c))
    universal-property-pushout-cogap-fiber-up-to-equiv {l} =
      universal-property-pushout-extension-by-equivalences
        ( horizontal-map-span-cogap-fiber)
        ( vertical-map-span-cogap-fiber)
        ( u)
        ( v)
        ( map-equiv i)
        ( map-equiv j)
        ( map-equiv k)
        ( pr1 ( universal-property-pushout-cogap-fiber {l}))
        ( pr2 universal-property-pushout-cogap-fiber)
        ( coh-l)
        ( coh-r)
        ( is-equiv-map-equiv i)
        ( is-equiv-map-equiv j)
        ( is-equiv-map-equiv k)
```

### Swapping a pushout cocone yields another pushout cocone

```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

  universal-property-pushout-swap-cocone-universal-property-pushout :
    universal-property-pushout f g c ā†’
    universal-property-pushout g f (swap-cocone f g X c)
  universal-property-pushout-swap-cocone-universal-property-pushout up Y =
    is-equiv-equiv'
      ( id-equiv)
      ( equiv-swap-cocone f g Y)
      ( Ī» h ā†’
        eq-htpy-cocone g f
          ( swap-cocone f g Y (cocone-map f g c h))
          ( cocone-map g f (swap-cocone f g X c) h)
          ( ( refl-htpy) ,
            ( refl-htpy) ,
            ( Ī» s ā†’
              right-unit āˆ™ inv (ap-inv h (coherence-square-cocone f g c s)))))
      ( up Y)

  is-pushout-swap-cocone-is-pushout :
    is-pushout f g c ā†’ is-pushout g f (swap-cocone f g X c)
  is-pushout-swap-cocone-is-pushout po =
    is-pushout-universal-property-pushout g f
      ( swap-cocone f g X c)
      ( universal-property-pushout-swap-cocone-universal-property-pushout
        ( universal-property-pushout-is-pushout f g c po))
```