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