# Equivalences of span diagrams on families of types ```agda module foundation.equivalences-span-diagrams-families-of-types where ``` <details><summary>Imports</summary> ```agda 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 ``` </details> ## Idea An {{#concept "equivalence of span diagrams on families of types" Agda=equiv-span-diagram-type-family}} from a [span](foundation.spans-families-of-types.md) `(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](foundation-core.families-of-equivalences.md) `h : Aᵢ ≃ Bᵢ`, and an equivalence `e : S ≃ T` [equipped](foundation.structure.md) with a family of [homotopies](foundation-core.homotopies.md) witnessing that the square ```text e S -----> T | | fᵢ | | gᵢ ∨ ∨ Aᵢ ----> Bᵢ h ``` [commutes](foundation-core.commuting-squares-of-maps.md) for each `i : I`. ## Definitions ### Equivalences of span diagrams on families of types ```agda 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 ```agda 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 ``` ## See also - [Equivalences of spans on families of types](foundation.equivalences-spans-families-of-types.md)