This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Families of equivalences

module foundation.families-of-equivalences where

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

open import foundation-core.propositions

Idea

A family of equivalences is a family

  eᵢ : A i ≃ B i

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

Properties

Being a fiberwise equivalence is a proposition

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

  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