# Equivalences of span diagrams

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2024-01-28.

module foundation.equivalences-span-diagrams where

Imports
open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-arrows
open import foundation.equivalences-spans
open import foundation.fundamental-theorem-of-identity-types
open import foundation.morphisms-span-diagrams
open import foundation.morphisms-spans
open import foundation.operations-spans
open import foundation.propositions
open import foundation.span-diagrams
open import foundation.structure-identity-principle
open import foundation.type-arithmetic-dependent-pair-types
open import foundation.univalence
open import foundation.universe-levels

open import foundation-core.commuting-squares-of-maps
open import foundation-core.functoriality-dependent-pair-types
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families


## Idea

An equivalence of span diagrams from a span diagram A <-f- S -g-> B to a span diagram C <-h- T -k-> D consists of equivalences u : A ≃ C, v : B ≃ D, and w : S ≃ T equipped with two homotopies witnessing that the diagram

         f       g
A <----- S -----> B
|        |        |
u |        | w      | v
∨        ∨        ∨
C <----- T -----> D
h       k


## Definitions

### The predicate of being an equivalence of span diagrams

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

is-equiv-prop-hom-span-diagram : Prop (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
is-equiv-prop-hom-span-diagram =
product-Prop
( is-equiv-Prop (map-domain-hom-span-diagram 𝒮 𝒯 f))
( product-Prop
( is-equiv-Prop (map-codomain-hom-span-diagram 𝒮 𝒯 f))
( is-equiv-Prop (spanning-map-hom-span-diagram 𝒮 𝒯 f)))

is-equiv-hom-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
is-equiv-hom-span-diagram = type-Prop is-equiv-prop-hom-span-diagram

is-prop-is-equiv-hom-span-diagram : is-prop is-equiv-hom-span-diagram
is-prop-is-equiv-hom-span-diagram =
is-prop-type-Prop is-equiv-prop-hom-span-diagram


### Equivalences of span diagrams

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

equiv-span-diagram : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5 ⊔ l6)
equiv-span-diagram =
Σ ( domain-span-diagram 𝒮 ≃ domain-span-diagram 𝒯)
( λ e →
Σ ( codomain-span-diagram 𝒮 ≃ codomain-span-diagram 𝒯)
( λ f →
equiv-span
( concat-span (span-span-diagram 𝒮) (map-equiv e) (map-equiv f))
( span-span-diagram 𝒯)))

module _
(e : equiv-span-diagram)
where

equiv-domain-equiv-span-diagram :
domain-span-diagram 𝒮 ≃ domain-span-diagram 𝒯
equiv-domain-equiv-span-diagram = pr1 e

map-domain-equiv-span-diagram :
domain-span-diagram 𝒮 → domain-span-diagram 𝒯
map-domain-equiv-span-diagram = map-equiv equiv-domain-equiv-span-diagram

is-equiv-map-domain-equiv-span-diagram :
is-equiv map-domain-equiv-span-diagram
is-equiv-map-domain-equiv-span-diagram =
is-equiv-map-equiv equiv-domain-equiv-span-diagram

equiv-codomain-equiv-span-diagram :
codomain-span-diagram 𝒮 ≃ codomain-span-diagram 𝒯
equiv-codomain-equiv-span-diagram = pr1 (pr2 e)

map-codomain-equiv-span-diagram :
codomain-span-diagram 𝒮 → codomain-span-diagram 𝒯
map-codomain-equiv-span-diagram =
map-equiv equiv-codomain-equiv-span-diagram

is-equiv-map-codomain-equiv-span-diagram :
is-equiv map-codomain-equiv-span-diagram
is-equiv-map-codomain-equiv-span-diagram =
is-equiv-map-equiv equiv-codomain-equiv-span-diagram

equiv-span-equiv-span-diagram :
equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
equiv-span-equiv-span-diagram =
pr2 (pr2 e)

spanning-equiv-equiv-span-diagram :
spanning-type-span-diagram 𝒮 ≃ spanning-type-span-diagram 𝒯
spanning-equiv-equiv-span-diagram =
equiv-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

spanning-map-equiv-span-diagram :
spanning-type-span-diagram 𝒮 → spanning-type-span-diagram 𝒯
spanning-map-equiv-span-diagram =
map-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

is-equiv-spanning-map-equiv-span-diagram :
is-equiv spanning-map-equiv-span-diagram
is-equiv-spanning-map-equiv-span-diagram =
is-equiv-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

left-square-equiv-span-diagram :
coherence-square-maps
( spanning-map-equiv-span-diagram)
( left-map-span-diagram 𝒮)
( left-map-span-diagram 𝒯)
( map-domain-equiv-span-diagram)
left-square-equiv-span-diagram =
left-triangle-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

equiv-left-arrow-equiv-span-diagram :
equiv-arrow (left-map-span-diagram 𝒮) (left-map-span-diagram 𝒯)
pr1 equiv-left-arrow-equiv-span-diagram =
spanning-equiv-equiv-span-diagram
pr1 (pr2 equiv-left-arrow-equiv-span-diagram) =
equiv-domain-equiv-span-diagram
pr2 (pr2 equiv-left-arrow-equiv-span-diagram) =
left-square-equiv-span-diagram

right-square-equiv-span-diagram :
coherence-square-maps
( spanning-map-equiv-span-diagram)
( right-map-span-diagram 𝒮)
( right-map-span-diagram 𝒯)
( map-codomain-equiv-span-diagram)
right-square-equiv-span-diagram =
right-triangle-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

equiv-right-arrow-equiv-span-diagram :
equiv-arrow (right-map-span-diagram 𝒮) (right-map-span-diagram 𝒯)
pr1 equiv-right-arrow-equiv-span-diagram =
spanning-equiv-equiv-span-diagram
pr1 (pr2 equiv-right-arrow-equiv-span-diagram) =
equiv-codomain-equiv-span-diagram
pr2 (pr2 equiv-right-arrow-equiv-span-diagram) =
right-square-equiv-span-diagram

hom-span-equiv-span-diagram :
hom-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
hom-span-equiv-span-diagram =
hom-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-domain-equiv-span-diagram)
( map-codomain-equiv-span-diagram))
( span-span-diagram 𝒯)
( equiv-span-equiv-span-diagram)

hom-equiv-span-diagram : hom-span-diagram 𝒮 𝒯
pr1 hom-equiv-span-diagram = map-domain-equiv-span-diagram
pr1 (pr2 hom-equiv-span-diagram) = map-codomain-equiv-span-diagram
pr2 (pr2 hom-equiv-span-diagram) = hom-span-equiv-span-diagram

is-equiv-equiv-span-diagram :
is-equiv-hom-span-diagram 𝒮 𝒯 hom-equiv-span-diagram
pr1 is-equiv-equiv-span-diagram =
is-equiv-map-domain-equiv-span-diagram
pr1 (pr2 is-equiv-equiv-span-diagram) =
is-equiv-map-codomain-equiv-span-diagram
pr2 (pr2 is-equiv-equiv-span-diagram) =
is-equiv-spanning-map-equiv-span-diagram

compute-equiv-span-diagram :
Σ (hom-span-diagram 𝒮 𝒯) (is-equiv-hom-span-diagram 𝒮 𝒯) ≃
equiv-span-diagram
compute-equiv-span-diagram =
( equiv-tot
( λ e →
( equiv-tot
( λ f →
compute-equiv-span
( concat-span
( span-span-diagram 𝒮)
( map-equiv e)
( map-equiv f))
( span-span-diagram 𝒯))) ∘e
( interchange-Σ-Σ _))) ∘e
( interchange-Σ-Σ _)


### The identity equivalence of span diagrams

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

id-equiv-span-diagram : equiv-span-diagram 𝒮 𝒮
pr1 id-equiv-span-diagram = id-equiv
pr1 (pr2 id-equiv-span-diagram) = id-equiv
pr2 (pr2 id-equiv-span-diagram) = id-equiv-span (span-span-diagram 𝒮)


## Properties

### Extensionality of span diagrams

Equality of span diagrams is equivalent to equivalences of span diagrams.

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

equiv-eq-span-diagram :
(𝒯 : span-diagram l1 l2 l3) → 𝒮 ＝ 𝒯 → equiv-span-diagram 𝒮 𝒯
equiv-eq-span-diagram 𝒯 refl = id-equiv-span-diagram 𝒮

is-torsorial-equiv-span-diagram :
is-torsorial (equiv-span-diagram 𝒮)
is-torsorial-equiv-span-diagram =
is-torsorial-Eq-structure
( is-torsorial-equiv (domain-span-diagram 𝒮))
( domain-span-diagram 𝒮 , id-equiv)
( is-torsorial-Eq-structure
( is-torsorial-equiv (codomain-span-diagram 𝒮))
( codomain-span-diagram 𝒮 , id-equiv)
( is-torsorial-equiv-span (span-span-diagram 𝒮)))

is-equiv-equiv-eq-span-diagram :
(𝒯 : span-diagram l1 l2 l3) → is-equiv (equiv-eq-span-diagram 𝒯)
is-equiv-equiv-eq-span-diagram =
fundamental-theorem-id is-torsorial-equiv-span-diagram equiv-eq-span-diagram

extensionality-span-diagram :
(𝒯 : span-diagram l1 l2 l3) → (𝒮 ＝ 𝒯) ≃ equiv-span-diagram 𝒮 𝒯
pr1 (extensionality-span-diagram 𝒯) = equiv-eq-span-diagram 𝒯
pr2 (extensionality-span-diagram 𝒯) = is-equiv-equiv-eq-span-diagram 𝒯

eq-equiv-span-diagram :
(𝒯 : span-diagram l1 l2 l3) → equiv-span-diagram 𝒮 𝒯 → 𝒮 ＝ 𝒯
eq-equiv-span-diagram 𝒯 = map-inv-equiv (extensionality-span-diagram 𝒯)