# Morphisms of cospans

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-07-25.

module foundation.morphisms-cospans where

Imports
open import foundation.cartesian-product-types
open import foundation.cospans
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.commuting-triangles-of-maps


## Idea

Consider two cospans c := (X , f , g) and d := (Y , h , k) from A to B. A morphism of cospans from c to d consists of a map u : X → Y equipped with homotopies witnessing that the two triangles

      u              u
X ----> Y      X ----> Y
\     /        \     /
f \   / h      g \   / k
∨ ∨            ∨ ∨
A              B


## Definitions

### Morphisms of cospans

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
(c : cospan l3 A B) (d : cospan l4 A B)
where

coherence-hom-cospan :
(codomain-cospan c → codomain-cospan d) → UU (l1 ⊔ l2 ⊔ l4)
coherence-hom-cospan h =
( coherence-triangle-maps (left-map-cospan d) h (left-map-cospan c)) ×
( coherence-triangle-maps (right-map-cospan d) h (right-map-cospan c))

hom-cospan : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-cospan =
Σ ( codomain-cospan c → codomain-cospan d)
( coherence-hom-cospan)