# Base changes of span diagrams

Content created by Egbert Rijke.

Created on 2024-03-26.

module foundation.base-changes-span-diagrams where

Imports
open import foundation.cartesian-morphisms-arrows
open import foundation.cartesian-morphisms-span-diagrams
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

Consider a span diagram 𝒮 := (A <-f- S -g-> B). A base change of 𝒮 consists of a span diagram 𝒯 and a cartesian morphism of span diagrams 𝒯 → 𝒮.

## Definitions

### Base changes of span diagrams

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

base-change-span-diagram :
UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4 ⊔ lsuc l5 ⊔ lsuc l6)
base-change-span-diagram =
Σ (span-diagram l4 l5 l6) (λ 𝒯 → cartesian-hom-span-diagram 𝒯 𝒮)

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

span-diagram-base-change-span-diagram : span-diagram l4 l5 l6
span-diagram-base-change-span-diagram = pr1 f

domain-span-diagram-base-change-span-diagram : UU l4
domain-span-diagram-base-change-span-diagram =
domain-span-diagram span-diagram-base-change-span-diagram

codomain-span-diagram-base-change-span-diagram : UU l5
codomain-span-diagram-base-change-span-diagram =
codomain-span-diagram span-diagram-base-change-span-diagram

spanning-type-span-diagram-base-change-span-diagram : UU l6
spanning-type-span-diagram-base-change-span-diagram =
spanning-type-span-diagram span-diagram-base-change-span-diagram

left-map-span-diagram-base-change-span-diagram :
spanning-type-span-diagram-base-change-span-diagram →
domain-span-diagram-base-change-span-diagram
left-map-span-diagram-base-change-span-diagram =
left-map-span-diagram span-diagram-base-change-span-diagram

right-map-span-diagram-base-change-span-diagram :
spanning-type-span-diagram-base-change-span-diagram →
codomain-span-diagram-base-change-span-diagram
right-map-span-diagram-base-change-span-diagram =
right-map-span-diagram span-diagram-base-change-span-diagram

cartesian-hom-base-change-span-diagram :
cartesian-hom-span-diagram span-diagram-base-change-span-diagram 𝒮
cartesian-hom-base-change-span-diagram = pr2 f

hom-cartesian-hom-base-change-span-diagram :
hom-span-diagram span-diagram-base-change-span-diagram 𝒮
hom-cartesian-hom-base-change-span-diagram =
hom-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( cartesian-hom-base-change-span-diagram)

map-domain-cartesian-hom-base-change-span-diagram :
domain-span-diagram span-diagram-base-change-span-diagram →
domain-span-diagram 𝒮
map-domain-cartesian-hom-base-change-span-diagram =
map-domain-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)

map-codomain-cartesian-hom-base-change-span-diagram :
codomain-span-diagram span-diagram-base-change-span-diagram →
codomain-span-diagram 𝒮
map-codomain-cartesian-hom-base-change-span-diagram =
map-codomain-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)

spanning-map-cartesian-hom-base-change-span-diagram :
spanning-type-span-diagram span-diagram-base-change-span-diagram →
spanning-type-span-diagram 𝒮
spanning-map-cartesian-hom-base-change-span-diagram =
spanning-map-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)

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

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

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

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

is-cartesian-cartesian-hom-base-change-span-diagram :
is-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)
is-cartesian-cartesian-hom-base-change-span-diagram =
is-cartesian-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( cartesian-hom-base-change-span-diagram)

is-left-cartesian-cartesian-hom-base-change-span-diagram :
is-left-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)
is-left-cartesian-cartesian-hom-base-change-span-diagram =
is-left-cartesian-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( cartesian-hom-base-change-span-diagram)

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

is-right-cartesian-cartesian-hom-base-change-span-diagram :
is-right-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( hom-cartesian-hom-base-change-span-diagram)
is-right-cartesian-cartesian-hom-base-change-span-diagram =
is-right-cartesian-cartesian-hom-span-diagram
( span-diagram-base-change-span-diagram)
( 𝒮)
( cartesian-hom-base-change-span-diagram)

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