Morphisms of cospan diagrams

Content created by Egbert Rijke.

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

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
  |        |        |
  |        |        |
  V        V        V
  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