module Cat.Instances.Shape.Cospan where

The “cospan” category🔗

A cospan in a category C\mathcal{C} is a pair of morphisms afcgba \xrightarrow{f} c \xleftarrow{g} b with a common codomain. A limit over a diagram with cospan shape is called a pullback. Correspondingly, to encode such diagrams, we have a “cospan category” \bull \to \bull \leftarrow \bull. The dual of this category, which looks like \bull \leftarrow \bull \to \bull, is the “span” category. Colimits over a span are called pushouts.

data Cospan-ob  : Type  where
  cs-a cs-b cs-c : Cospan-ob 

Cospan-hom :  { ℓ′}  Cospan-ob   Cospan-ob   Type ℓ′
Cospan-hom cs-a cs-a = Lift _  -- identity on a
Cospan-hom cs-a cs-b = Lift _  -- no maps a → b
Cospan-hom cs-a cs-c = Lift _  -- one map a → c
Cospan-hom cs-b cs-a = Lift _  -- no maps b → a
Cospan-hom cs-b cs-b = Lift _  -- identity on b
Cospan-hom cs-b cs-c = Lift _  -- one map b → c
Cospan-hom cs-c cs-a = Lift _  -- no maps c → a
Cospan-hom cs-c cs-b = Lift _  -- no maps c → b
Cospan-hom cs-c cs-c = Lift _  -- identity on c

·→·←· ·←·→· :  {a b}  Precategory a b
·→·←· = precat where
  open Precategory

  compose :  {a b c}  Cospan-hom b c  Cospan-hom a b  Cospan-hom a c
  compose {cs-a} {cs-a} {cs-a} (lift tt) (lift tt) = lift tt
  compose {cs-a} {cs-a} {cs-c} (lift tt) (lift tt) = lift tt
  compose {cs-a} {cs-c} {cs-c} (lift tt) (lift tt) = lift tt
  compose {cs-b} {cs-b} {cs-b} (lift tt) (lift tt) = lift tt
  compose {cs-b} {cs-b} {cs-c} (lift tt) (lift tt) = lift tt
  compose {cs-b} {cs-c} {cs-c} (lift tt) (lift tt) = lift tt
  compose {cs-c} {cs-c} {cs-c} (lift tt) (lift tt) = lift tt

  precat : Precategory _ _
  precat .Ob = Cospan-ob _
  precat .Hom = Cospan-hom
  precat .Hom-set cs-a cs-a _ _ p q i j = lift tt
  precat .Hom-set cs-a cs-c _ _ p q i j = lift tt
  precat .Hom-set cs-b cs-b _ _ p q i j = lift tt
  precat .Hom-set cs-b cs-c _ _ p q i j = lift tt
  precat .Hom-set cs-c cs-c _ _ p q i j = lift tt
  precat .id {cs-a} = lift tt
  precat .id {cs-b} = lift tt
  precat .id {cs-c} = lift tt
  precat ._∘_ = compose
  precat .idr {cs-a} {cs-a} _ i = lift tt
  precat .idr {cs-a} {cs-c} _ i = lift tt
  precat .idr {cs-b} {cs-b} _ i = lift tt
  precat .idr {cs-b} {cs-c} _ i = lift tt
  precat .idr {cs-c} {cs-c} _ i = lift tt
  precat .idl {cs-a} {cs-a} _ i = lift tt
  precat .idl {cs-a} {cs-c} _ i = lift tt
  precat .idl {cs-b} {cs-b} _ i = lift tt
  precat .idl {cs-b} {cs-c} _ i = lift tt
  precat .idl {cs-c} {cs-c} _ i = lift tt
  precat .assoc {cs-a} {cs-a} {cs-a} {cs-a} _ _ _ i = lift tt
  precat .assoc {cs-a} {cs-a} {cs-a} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-a} {cs-a} {cs-c} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-a} {cs-c} {cs-c} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-b} {cs-b} {cs-b} {cs-b} _ _ _ i = lift tt
  precat .assoc {cs-b} {cs-b} {cs-b} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-b} {cs-b} {cs-c} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-b} {cs-c} {cs-c} {cs-c} _ _ _ i = lift tt
  precat .assoc {cs-c} {cs-c} {cs-c} {cs-c} _ _ _ i = lift tt

·←·→· = ·→·←· ^op

Converting a pair of morphisms with common codomain to a cospan-shaped diagram is straightforward:

module _ x y {o } {C : Precategory o } where
  open Precategory C
  open Functor

  cospan→cospan-diagram :  {a b c}  Hom a c  Hom b c  Functor (·→·←· {x} {y}) C
  cospan→cospan-diagram f g = funct where
    funct : Functor _ _
    funct .F₀ cs-a = _
    funct .F₀ cs-b = _
    funct .F₀ cs-c = _
    funct .F₁ {cs-a} {cs-c} _ = f
    funct .F₁ {cs-b} {cs-c} _ = g