Morphisms of cospan diagrams

Content created by Egbert Rijke.

Created on 2024-01-28.
Last modified on 2024-04-25.

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

open import foundation-core.cartesian-product-types
open import foundation-core.function-types
open import foundation-core.homotopies

Idea

A morphism of cospan diagrams is a commuting diagram of the form

  A -----> X <----- B
  |        |        |
  |        |        |
  ∨        ∨        ∨
  A' ----> X' <---- B'.

Definitions

Morphisms of cospan diagrams

hom-cospan-diagram :
  {l1 l2 l3 l1' l2' l3' : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X') →
  UU (l1 ⊔ l2 ⊔ l3 ⊔ l1' ⊔ l2' ⊔ l3')
hom-cospan-diagram {A = A} {B} {X} f g {A'} {B'} {X'} f' g' =
  Σ ( A → A')
    ( λ hA →
      Σ ( B → B')
        ( λ hB →
          Σ ( X → X')
            ( λ hX → (f' ∘ hA ~ hX ∘ f) × (g' ∘ hB ~ hX ∘ g))))

Identity morphisms of cospan diagrams

id-hom-cospan-diagram :
  {l1 l2 l3 l1' l2' l3' : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) →
  hom-cospan-diagram f g f g
pr1 (id-hom-cospan-diagram f g) = id
pr1 (pr2 (id-hom-cospan-diagram f g)) = id
pr1 (pr2 (pr2 (id-hom-cospan-diagram f g))) = id
pr1 (pr2 (pr2 (pr2 (id-hom-cospan-diagram f g)))) = refl-htpy
pr2 (pr2 (pr2 (pr2 (id-hom-cospan-diagram f g)))) = refl-htpy

Rotating cospan diagrams of cospan diagrams

cospan-hom-cospan-diagram-rotate :
  {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X')
  {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''}
  (f'' : A'' → X'') (g'' : B'' → X'')
  (h : hom-cospan-diagram f' g' f g) (h' : hom-cospan-diagram f'' g'' f g) →
  hom-cospan-diagram (pr1 h) (pr1 h') (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h')))
pr1
  ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g''
    ( hA , hB , hX , HA , HB)
    ( hA' , hB' , hX' , HA' , HB')) = f'
pr1
  ( pr2
    ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g''
      ( hA , hB , hX , HA , HB)
      ( hA' , hB' , hX' , HA' , HB'))) = f''
pr1
  ( pr2
    ( pr2
      ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g''
        ( hA , hB , hX , HA , HB)
        ( hA' , hB' , hX' , HA' , HB')))) = f
pr1
  ( pr2
    ( pr2
      ( pr2
        ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g''
          ( hA , hB , hX , HA , HB)
          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA
pr2
  ( pr2
    ( pr2
      ( pr2
        ( cospan-hom-cospan-diagram-rotate f g f' g' f'' g''
          ( hA , hB , hX , HA , HB)
          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HA'

cospan-hom-cospan-diagram-rotate' :
  {l1 l2 l3 l1' l2' l3' l1'' l2'' l3'' : Level}
  {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X)
  {A' : UU l1'} {B' : UU l2'} {X' : UU l3'} (f' : A' → X') (g' : B' → X')
  {A'' : UU l1''} {B'' : UU l2''} {X'' : UU l3''}
  (f'' : A'' → X'') (g'' : B'' → X'')
  (h : hom-cospan-diagram f' g' f g) (h' : hom-cospan-diagram f'' g'' f g) →
  hom-cospan-diagram
    (pr1 (pr2 h)) (pr1 (pr2 h')) (pr1 (pr2 (pr2 h))) (pr1 (pr2 (pr2 h')))
pr1
  ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g''
    ( hA , hB , hX , HA , HB)
    ( hA' , hB' , hX' , HA' , HB')) = g'
pr1
  ( pr2
    ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g''
      ( hA , hB , hX , HA , HB)
      ( hA' , hB' , hX' , HA' , HB'))) = g''
pr1
  ( pr2
    ( pr2
      ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g''
        ( hA , hB , hX , HA , HB)
        ( hA' , hB' , hX' , HA' , HB')))) = g
pr1
  ( pr2
    ( pr2
      ( pr2
        ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g''
          ( hA , hB , hX , HA , HB)
          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB
pr2
  ( pr2
    ( pr2
      ( pr2
        ( cospan-hom-cospan-diagram-rotate' f g f' g' f'' g''
          ( hA , hB , hX , HA , HB)
          ( hA' , hB' , hX' , HA' , HB'))))) = inv-htpy HB'

Recent changes