Cospan diagrams

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-01-28.
Last modified on 2024-10-27.

module foundation.cospan-diagrams where
Imports 
open import foundation.cospans
open import foundation.dependent-pair-types
open import foundation.universe-levels

Idea

A cospan diagram consists of two types A and B and a cospan A -f-> X <-g- B between them.

Definitions

Cospan diagrams

cospan-diagram :
  (l1 l2 l3 : Level) → UU (lsuc l1 ⊔ lsuc l2 ⊔ lsuc l3)
cospan-diagram l1 l2 l3 =
  Σ (UU l1) (λ A → Σ (UU l2) (cospan l3 A))

module _
  {l1 l2 l3 : Level} (c : cospan-diagram l1 l2 l3)
  where

  left-type-cospan-diagram : UU l1
  left-type-cospan-diagram = pr1 c

  right-type-cospan-diagram : UU l2
  right-type-cospan-diagram = pr1 (pr2 c)

  cospan-cospan-diagram :
    cospan l3 left-type-cospan-diagram right-type-cospan-diagram
  cospan-cospan-diagram = pr2 (pr2 c)

  cospanning-type-cospan-diagram : UU l3
  cospanning-type-cospan-diagram = codomain-cospan cospan-cospan-diagram

  left-map-cospan-diagram :
    left-type-cospan-diagram → cospanning-type-cospan-diagram
  left-map-cospan-diagram = left-map-cospan cospan-cospan-diagram

  right-map-cospan-diagram :
    right-type-cospan-diagram → cospanning-type-cospan-diagram
  right-map-cospan-diagram = right-map-cospan cospan-cospan-diagram

The identity cospan diagram

id-cospan-diagram : {l : Level} → UU l → cospan-diagram l l l
id-cospan-diagram A = (A , A , id-cospan A)

The swapping operation on cospan diagrams

swap-cospan-diagram :
  {l1 l2 l3 : Level} → cospan-diagram l1 l2 l3 → cospan-diagram l2 l1 l3
swap-cospan-diagram (A , B , c) = (B , A , swap-cospan c)

Recent changes