# Morphisms of spans

Content created by Egbert Rijke.

Created on 2024-01-28.

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


## 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)