module Cat.Instances.Shape.Cospan where
The “cospan” category🔗
A cospan in a category is a pair of morphisms 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” . The dual of this category, which looks like , 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 instance Finite-Cospan-ob : ∀ {ℓ} → Finite (Cospan-ob ℓ) Finite-Cospan-ob = fin {cardinality = 3} (inc (Iso→Equiv i)) where i : Iso _ _ i .fst cs-a = 0 i .fst cs-b = 1 i .fst cs-c = 2 i .snd .is-iso.inv fzero = cs-a i .snd .is-iso.inv (fsuc fzero) = cs-b i .snd .is-iso.inv (fsuc (fsuc fzero)) = cs-c i .snd .is-iso.rinv fzero = refl i .snd .is-iso.rinv (fsuc fzero) = refl i .snd .is-iso.rinv (fsuc (fsuc fzero)) = refl i .snd .is-iso.linv cs-a = refl i .snd .is-iso.linv cs-b = refl i .snd .is-iso.linv cs-c = refl ·→·←·-finite : ∀ {a b} → is-finite-precategory (·→·←· {a} {b}) ·→·←·-finite = finite-cat-hom λ where cs-a cs-a → auto cs-a cs-b → auto cs-a cs-c → auto cs-b cs-a → auto cs-b cs-b → auto cs-b cs-c → auto cs-c cs-a → auto cs-c cs-b → auto cs-c cs-c → auto
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
funct .F₁ {cs-a} {cs-a} _ = _ funct .F₁ {cs-b} {cs-b} _ = _ funct .F₁ {cs-c} {cs-c} _ = _ funct .F-id {cs-a} = refl funct .F-id {cs-b} = refl funct .F-id {cs-c} = refl funct .F-∘ {cs-a} {cs-a} {cs-a} _ _ i = idl id (~ i) funct .F-∘ {cs-a} {cs-a} {cs-c} _ _ i = idr f (~ i) funct .F-∘ {cs-a} {cs-c} {cs-c} _ _ i = idl f (~ i) funct .F-∘ {cs-b} {cs-b} {cs-b} _ _ i = idl id (~ i) funct .F-∘ {cs-b} {cs-b} {cs-c} _ _ i = idr g (~ i) funct .F-∘ {cs-b} {cs-c} {cs-c} _ _ i = idl g (~ i) funct .F-∘ {cs-c} {cs-c} {cs-c} _ _ i = idl id (~ i) span→span-diagram : ∀ {a b c} → Hom a b → Hom a c → Functor (·←·→· {x} {y}) C span→span-diagram {a} {b} {c} f g = funct where funct : Functor _ _ funct .F₀ cs-a = _ funct .F₀ cs-b = _ funct .F₀ cs-c = _ funct .F₁ {cs-a} {cs-a} _ = id funct .F₁ {cs-b} {cs-b} _ = id funct .F₁ {cs-c} {cs-a} _ = g funct .F₁ {cs-c} {cs-b} _ = f funct .F₁ {cs-c} {cs-c} _ = id funct .F-id {cs-a} = refl funct .F-id {cs-b} = refl funct .F-id {cs-c} = refl funct .F-∘ {cs-a} {cs-a} {cs-a} _ _ i = idl id (~ i) funct .F-∘ {cs-b} {cs-b} {cs-b} _ _ i = idl id (~ i) funct .F-∘ {cs-c} {cs-a} {cs-a} _ _ i = idl g (~ i) funct .F-∘ {cs-c} {cs-b} {cs-b} _ _ i = idl f (~ i) funct .F-∘ {cs-c} {cs-c} {cs-a} _ _ i = idr g (~ i) funct .F-∘ {cs-c} {cs-c} {cs-b} _ _ i = idr f (~ i) funct .F-∘ {cs-c} {cs-c} {cs-c} _ _ i = idr id (~ i)