Morphisms of spans

Content created by Egbert Rijke.

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

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

open import foundation-core.cartesian-product-types
open import foundation-core.commuting-squares-of-maps
open import foundation-core.commuting-triangles-of-maps
open import foundation-core.operations-spans

Idea

A morphism of spans from a span A <-f- S -g-> B to a span A <-h- T -k-> B consists of a map w : S → T equipped with two homotopies witnessing that the diagram

             S
           / | \
        f /  |  \ h
         ∨   |   ∨
        A    |w   B
         ∧   |   ∧
        h \  |  / k
           \ ∨ /
             T

commutes.

Definitions

Morphisms between spans

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
  (s : span l3 A B) (t : span l4 A B)
  where

  left-coherence-hom-span :
    (spanning-type-span s → spanning-type-span t) → UU (l1 ⊔ l3)
  left-coherence-hom-span =
    coherence-triangle-maps (left-map-span s) (left-map-span t)

  right-coherence-hom-span :
    (spanning-type-span s → spanning-type-span t) → UU (l2 ⊔ l3)
  right-coherence-hom-span =
    coherence-triangle-maps (right-map-span s) (right-map-span t)

  coherence-hom-span :
    (spanning-type-span s → spanning-type-span t) → UU (l1 ⊔ l2 ⊔ l3)
  coherence-hom-span f = left-coherence-hom-span f × right-coherence-hom-span f

  hom-span : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4)
  hom-span = Σ (spanning-type-span s → spanning-type-span t) coherence-hom-span

module _
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2}
  (s : span l3 A B) (t : span l4 A B) (f : hom-span s t)
  where

  map-hom-span : spanning-type-span s → spanning-type-span t
  map-hom-span = pr1 f

  left-triangle-hom-span : left-coherence-hom-span s t map-hom-span
  left-triangle-hom-span = pr1 (pr2 f)

  right-triangle-hom-span : right-coherence-hom-span s t map-hom-span
  right-triangle-hom-span = pr2 (pr2 f)

Recent changes