# Families of equivalences

Content created by Egbert Rijke and Raymond Baker.

Created on 2023-12-05.

module foundation-core.families-of-equivalences where

Imports
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.type-theoretic-principle-of-choice


## Idea

A family of equivalences is a family

  eᵢ : A i ≃ B i


of equivalences. Families of equivalences are also called fiberwise equivalences.

## Definitions

### The predicate of being a fiberwise equivalence

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
where

is-fiberwise-equiv : (f : (x : A) → B x → C x) → UU (l1 ⊔ l2 ⊔ l3)
is-fiberwise-equiv f = (x : A) → is-equiv (f x)


### Fiberwise equivalences

module _
{l1 l2 l3 : Level} {A : UU l1}
where

fiberwise-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
fiberwise-equiv B C = Σ ((x : A) → B x → C x) is-fiberwise-equiv

map-fiberwise-equiv :
{B : A → UU l2} {C : A → UU l3} →
fiberwise-equiv B C → (a : A) → B a → C a
map-fiberwise-equiv = pr1

is-fiberwise-equiv-fiberwise-equiv :
{B : A → UU l2} {C : A → UU l3} →
(e : fiberwise-equiv B C) →
is-fiberwise-equiv (map-fiberwise-equiv e)
is-fiberwise-equiv-fiberwise-equiv = pr2


### Families of equivalences

module _
{l1 l2 l3 : Level} {A : UU l1}
where

fam-equiv : (B : A → UU l2) (C : A → UU l3) → UU (l1 ⊔ l2 ⊔ l3)
fam-equiv B C = (x : A) → B x ≃ C x

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
(e : fam-equiv B C)
where

map-fam-equiv : (x : A) → B x → C x
map-fam-equiv x = map-equiv (e x)

is-equiv-map-fam-equiv : is-fiberwise-equiv map-fam-equiv
is-equiv-map-fam-equiv x = is-equiv-map-equiv (e x)


## Properties

### Families of equivalences are equivalent to fiberwise equivalences

equiv-fiberwise-equiv-fam-equiv :
{l1 l2 l3 : Level} {A : UU l1} (B : A → UU l2) (C : A → UU l3) →
fam-equiv B C ≃ fiberwise-equiv B C
equiv-fiberwise-equiv-fam-equiv B C = distributive-Π-Σ