Univalent type families

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.

Created on 2022-03-03.
Last modified on 2023-09-11.

module foundation.univalent-type-families where
Imports 
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.identity-types

Idea

A type family B over A is said to be univalent if the map

  equiv-tr : (Id x y) → (B x ≃ B y)

is an equivalence for every x y : A.

Definition

is-univalent :
  {l1 l2 : Level} {A : UU l1} → (A → UU l2) → UU (l1 ⊔ l2)
is-univalent {A = A} B = (x y : A) → is-equiv (λ (p : x ＝ y) → equiv-tr B p)

Recent changes