# Cartesian morphisms of span diagrams

Content created by Egbert Rijke.

Created on 2024-03-26.

module foundation.cartesian-morphisms-span-diagrams where

Imports
open import foundation.cartesian-morphisms-arrows
open import foundation.cartesian-product-types
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.morphisms-arrows
open import foundation.morphisms-span-diagrams
open import foundation.span-diagrams
open import foundation.universe-levels


## Idea

A morphism α : 𝒮 → 𝒯 of span diagrams is said to be cartesian if the two squares in the diagram

       h       k
C <----- T -----> D
|      ⌞ | ⌟      |
|        |        |
∨        ∨        ∨
A <----- S -----> B
f       g


are pullback squares.

## Definitions

### The predicate of being a left cartesian morphism of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6) (α : hom-span-diagram 𝒮 𝒯)
where

is-left-cartesian-hom-span-diagram : UU (l1 ⊔ l3 ⊔ l4 ⊔ l6)
is-left-cartesian-hom-span-diagram =
is-cartesian-hom-arrow
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
( left-hom-arrow-hom-span-diagram 𝒮 𝒯 α)


### Left cartesian morphisms of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6)
where

left-cartesian-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
left-cartesian-hom-span-diagram =
Σ (hom-span-diagram 𝒮 𝒯) (is-left-cartesian-hom-span-diagram 𝒮 𝒯)

module _
(h : left-cartesian-hom-span-diagram)
where

hom-left-cartesian-hom-span-diagram : hom-span-diagram 𝒮 𝒯
hom-left-cartesian-hom-span-diagram = pr1 h

map-domain-left-cartesian-hom-span-diagram :
domain-span-diagram 𝒮 → domain-span-diagram 𝒯
map-domain-left-cartesian-hom-span-diagram =
map-domain-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

map-codomain-left-cartesian-hom-span-diagram :
codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯
map-codomain-left-cartesian-hom-span-diagram =
map-codomain-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

spanning-map-left-cartesian-hom-span-diagram :
spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯
spanning-map-left-cartesian-hom-span-diagram =
spanning-map-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

left-square-left-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-left-cartesian-hom-span-diagram)
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
( map-domain-left-cartesian-hom-span-diagram)
left-square-left-cartesian-hom-span-diagram =
left-square-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

left-hom-arrow-left-cartesian-hom-span-diagram :
hom-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯)
left-hom-arrow-left-cartesian-hom-span-diagram =
left-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

right-square-left-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-left-cartesian-hom-span-diagram)
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
( map-codomain-left-cartesian-hom-span-diagram)
right-square-left-cartesian-hom-span-diagram =
right-square-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

right-hom-arrow-left-cartesian-hom-span-diagram :
hom-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯)
right-hom-arrow-left-cartesian-hom-span-diagram =
right-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram

is-left-cartesian-left-cartesian-hom-span-diagram :
is-left-cartesian-hom-span-diagram 𝒮 𝒯 hom-left-cartesian-hom-span-diagram
is-left-cartesian-left-cartesian-hom-span-diagram = pr2 h


### The predicate of being a right cartesian morphism of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6) (α : hom-span-diagram 𝒮 𝒯)
where

is-right-cartesian-hom-span-diagram : UU (l2 ⊔ l3 ⊔ l5 ⊔ l6)
is-right-cartesian-hom-span-diagram =
is-cartesian-hom-arrow
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
( right-hom-arrow-hom-span-diagram 𝒮 𝒯 α)


### Right cartesian morphisms of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6)
where

right-cartesian-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
right-cartesian-hom-span-diagram =
Σ (hom-span-diagram 𝒮 𝒯) (is-right-cartesian-hom-span-diagram 𝒮 𝒯)

module _
(h : right-cartesian-hom-span-diagram)
where

hom-right-cartesian-hom-span-diagram : hom-span-diagram 𝒮 𝒯
hom-right-cartesian-hom-span-diagram = pr1 h

map-domain-right-cartesian-hom-span-diagram :
domain-span-diagram 𝒮 → domain-span-diagram 𝒯
map-domain-right-cartesian-hom-span-diagram =
map-domain-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

map-codomain-right-cartesian-hom-span-diagram :
codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯
map-codomain-right-cartesian-hom-span-diagram =
map-codomain-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

spanning-map-right-cartesian-hom-span-diagram :
spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯
spanning-map-right-cartesian-hom-span-diagram =
spanning-map-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

left-square-right-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-right-cartesian-hom-span-diagram)
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
( map-domain-right-cartesian-hom-span-diagram)
left-square-right-cartesian-hom-span-diagram =
left-square-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

left-hom-arrow-right-cartesian-hom-span-diagram :
hom-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯)
left-hom-arrow-right-cartesian-hom-span-diagram =
left-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

right-square-right-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-right-cartesian-hom-span-diagram)
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
( map-codomain-right-cartesian-hom-span-diagram)
right-square-right-cartesian-hom-span-diagram =
right-square-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

right-hom-arrow-right-cartesian-hom-span-diagram :
hom-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯)
right-hom-arrow-right-cartesian-hom-span-diagram =
right-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-right-cartesian-hom-span-diagram

is-right-cartesian-right-cartesian-hom-span-diagram :
is-right-cartesian-hom-span-diagram 𝒮 𝒯
( hom-right-cartesian-hom-span-diagram)
is-right-cartesian-right-cartesian-hom-span-diagram = pr2 h


### The predicate of being a cartesian morphism of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6) (α : hom-span-diagram 𝒮 𝒯)
where

is-cartesian-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
is-cartesian-hom-span-diagram =
is-left-cartesian-hom-span-diagram 𝒮 𝒯 α ×
is-right-cartesian-hom-span-diagram 𝒮 𝒯 α


### Cartesian morphisms of span diagrams

module _
{l1 l2 l3 l4 l5 l6 : Level} (𝒮 : span-diagram l1 l2 l3)
(𝒯 : span-diagram l4 l5 l6)
where

cartesian-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
cartesian-hom-span-diagram =
Σ (hom-span-diagram 𝒮 𝒯) (is-cartesian-hom-span-diagram 𝒮 𝒯)

module _
(h : cartesian-hom-span-diagram)
where

hom-cartesian-hom-span-diagram : hom-span-diagram 𝒮 𝒯
hom-cartesian-hom-span-diagram = pr1 h

map-domain-cartesian-hom-span-diagram :
domain-span-diagram 𝒮 → domain-span-diagram 𝒯
map-domain-cartesian-hom-span-diagram =
map-domain-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

map-codomain-cartesian-hom-span-diagram :
codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯
map-codomain-cartesian-hom-span-diagram =
map-codomain-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

spanning-map-cartesian-hom-span-diagram :
spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯
spanning-map-cartesian-hom-span-diagram =
spanning-map-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

left-square-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-cartesian-hom-span-diagram)
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
( map-domain-cartesian-hom-span-diagram)
left-square-cartesian-hom-span-diagram =
left-square-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

left-hom-arrow-cartesian-hom-span-diagram :
hom-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯)
left-hom-arrow-cartesian-hom-span-diagram =
left-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

right-square-cartesian-hom-span-diagram :
coherence-square-maps
( spanning-map-cartesian-hom-span-diagram)
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
( map-codomain-cartesian-hom-span-diagram)
right-square-cartesian-hom-span-diagram =
right-square-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

right-hom-arrow-cartesian-hom-span-diagram :
hom-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯)
right-hom-arrow-cartesian-hom-span-diagram =
right-hom-arrow-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram

is-cartesian-cartesian-hom-span-diagram :
is-cartesian-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram
is-cartesian-cartesian-hom-span-diagram = pr2 h

is-left-cartesian-cartesian-hom-span-diagram :
is-left-cartesian-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram
is-left-cartesian-cartesian-hom-span-diagram =
pr1 is-cartesian-cartesian-hom-span-diagram

left-cartesian-hom-arrow-cartesian-hom-span-diagram :
cartesian-hom-arrow
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
pr1 left-cartesian-hom-arrow-cartesian-hom-span-diagram =
left-hom-arrow-cartesian-hom-span-diagram
pr2 left-cartesian-hom-arrow-cartesian-hom-span-diagram =
is-left-cartesian-cartesian-hom-span-diagram

is-right-cartesian-cartesian-hom-span-diagram :
is-right-cartesian-hom-span-diagram 𝒮 𝒯 hom-cartesian-hom-span-diagram
is-right-cartesian-cartesian-hom-span-diagram =
pr2 is-cartesian-cartesian-hom-span-diagram

right-cartesian-hom-arrow-cartesian-hom-span-diagram :
cartesian-hom-arrow
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
pr1 right-cartesian-hom-arrow-cartesian-hom-span-diagram =
right-hom-arrow-cartesian-hom-span-diagram
pr2 right-cartesian-hom-arrow-cartesian-hom-span-diagram =
is-right-cartesian-cartesian-hom-span-diagram