# Equivalences of span diagrams on families of types

Content created by Egbert Rijke.

Created on 2024-01-28.

module foundation.equivalences-span-diagrams-families-of-types where

Imports
open import foundation.commuting-squares-of-maps
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.equivalences-spans-families-of-types
open import foundation.homotopies
open import foundation.operations-spans-families-of-types
open import foundation.span-diagrams-families-of-types
open import foundation.universe-levels


## Idea

An equivalence of span diagrams on families of types from a span (A , s) of families of types indexed by a type I to a span (B , t) indexed by I consists of a family of equivalences h : Aᵢ ≃ Bᵢ, and an equivalence e : S ≃ T equipped with a family of homotopies witnessing that the square

         e
S -----> T
|        |
fᵢ |        | gᵢ
∨        ∨
Aᵢ ----> Bᵢ
h


commutes for each i : I.

## Definitions

### Equivalences of span diagrams on families of types

module _
{l1 l2 l3 l4 l5 : Level} {I : UU l1}
(S : span-diagram-type-family l2 l3 I)
(T : span-diagram-type-family l4 l5 I)
where

equiv-span-diagram-type-family : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5)
equiv-span-diagram-type-family =
Σ ( (i : I) →
family-span-diagram-type-family S i ≃
family-span-diagram-type-family T i)
( λ e →
equiv-span-type-family
( concat-span-hom-family-of-types
( span-span-diagram-type-family S)
( λ i → map-equiv (e i)))
( span-span-diagram-type-family T))

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

equiv-family-equiv-span-diagram-type-family :
(i : I) →
family-span-diagram-type-family S i ≃
family-span-diagram-type-family T i
equiv-family-equiv-span-diagram-type-family = pr1 e

map-family-equiv-span-diagram-type-family :
(i : I) →
family-span-diagram-type-family S i →
family-span-diagram-type-family T i
map-family-equiv-span-diagram-type-family i =
map-equiv (equiv-family-equiv-span-diagram-type-family i)

equiv-span-equiv-span-diagram-type-family :
equiv-span-type-family
( concat-span-hom-family-of-types
( span-span-diagram-type-family S)
( map-family-equiv-span-diagram-type-family))
( span-span-diagram-type-family T)
equiv-span-equiv-span-diagram-type-family = pr2 e

spanning-equiv-equiv-span-diagram-type-family :
spanning-type-span-diagram-type-family S ≃
spanning-type-span-diagram-type-family T
spanning-equiv-equiv-span-diagram-type-family =
equiv-equiv-span-type-family
( concat-span-hom-family-of-types
( span-span-diagram-type-family S)
( map-family-equiv-span-diagram-type-family))
( span-span-diagram-type-family T)
( equiv-span-equiv-span-diagram-type-family)

spanning-map-equiv-span-diagram-type-family :
spanning-type-span-diagram-type-family S →
spanning-type-span-diagram-type-family T
spanning-map-equiv-span-diagram-type-family =
map-equiv spanning-equiv-equiv-span-diagram-type-family

coherence-square-equiv-span-diagram-type-family :
(i : I) →
coherence-square-maps
( spanning-map-equiv-span-diagram-type-family)
( map-span-diagram-type-family S i)
( map-span-diagram-type-family T i)
( map-family-equiv-span-diagram-type-family i)
coherence-square-equiv-span-diagram-type-family =
triangle-equiv-span-type-family
( concat-span-hom-family-of-types
( span-span-diagram-type-family S)
( map-family-equiv-span-diagram-type-family))
( span-span-diagram-type-family T)
( equiv-span-equiv-span-diagram-type-family)


### Identity equivalences of spans diagrams on families of types

module _
{l1 l2 l3 : Level} {I : UU l1} {𝒮 : span-diagram-type-family l2 l3 I}
where

id-equiv-span-diagram-type-family :
equiv-span-diagram-type-family 𝒮 𝒮
pr1 id-equiv-span-diagram-type-family i = id-equiv
pr1 (pr2 id-equiv-span-diagram-type-family) = id-equiv
pr2 (pr2 id-equiv-span-diagram-type-family) i = refl-htpy