This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Morphisms of cospans

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

commute.

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)