Families of equivalences

Content created by Egbert Rijke and Raymond Baker.

Created on 2023-11-24.
Last modified on 2023-12-05.

module foundation.families-of-equivalences where

open import foundation-core.families-of-equivalences public
open import foundation.equivalences
open import foundation.universe-levels

open import foundation-core.propositions


A family of equivalences is a family

  eᵢ : A i ≃ B i

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


Being a fiberwise equivalence is a proposition

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

  is-property-is-fiberwise-equiv :
    (f : (a : A)  B a  C a)  is-prop (is-fiberwise-equiv f)
  is-property-is-fiberwise-equiv f =
    is-prop-Π  a  is-property-is-equiv (f a))

See also

Recent changes