open import Cat.Prelude

module Cat.Instances.Shape.Cospan where


# The “cospan” category🔗

A cospan in a category $\mathcal{C}$ is a pair of morphisms $a {\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


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