# Univalent type families

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

Created on 2022-03-03.

module foundation.univalent-type-families where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-systems
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.subuniverses
open import foundation.transport-along-identifications
open import foundation.univalence
open import foundation.universal-property-identity-systems
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.sections
open import foundation-core.torsorial-type-families


## Idea

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

  equiv-tr B : x ＝ y → B x ≃ B y


is an equivalence for every x y : A. By the univalence axiom, this is equivalent to the type family B being an embedding considered as a map.

## Definition

### The predicate on type families of being univalent

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)

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

is-prop-is-univalent : is-prop (is-univalent B)
is-prop-is-univalent =
is-prop-iterated-Π 2 (λ x y → is-property-is-equiv (equiv-tr B))

is-univalent-Prop : Prop (l1 ⊔ l2)
pr1 is-univalent-Prop = is-univalent B
pr2 is-univalent-Prop = is-prop-is-univalent


### Univalent type families

univalent-type-family :
{l1 : Level} (l2 : Level) (A : UU l1) → UU (l1 ⊔ lsuc l2)
univalent-type-family l2 A = Σ (A → UU l2) is-univalent


## Properties

### The univalence axiom states that the identity family id : 𝒰 → 𝒰 is univalent

is-univalent-UU :
(l : Level) → is-univalent (id {A = UU l})
is-univalent-UU l = univalence


### Assuming the univalence axiom, type families are univalent if and only if they are embeddings as maps

Proof: We have the commuting triangle of maps

                ap B
(x ＝ y) -----> (B x ＝ B y)
\               /
\             /
equiv-tr B \           / equiv-eq
∨         ∨
(B x ≃ B y)


where the right edge is an equivalence by the univalence axiom. Hence, the top map is an equivalence if and only if the left map is.

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

abstract
is-emb-is-univalent :
is-univalent B → is-emb B
is-emb-is-univalent U x y =
is-equiv-top-map-triangle
( equiv-tr B)
( equiv-eq)
( ap B)
( λ where refl → refl)
( univalence (B x) (B y))
( U x y)

is-univalent-is-emb :
is-emb B → is-univalent B
is-univalent-is-emb is-emb-B x y =
is-equiv-left-map-triangle
( equiv-tr B)
( equiv-eq)
( ap B)
( λ where refl → refl)
( is-emb-B x y)
( univalence (B x) (B y))


### Univalent type families satisfy equivalence induction

module _
{l1 l2 : Level} {A : UU l1} {B : A → UU l2}
(U : is-univalent B)
where

is-torsorial-fam-equiv-is-univalent :
{x : A} → is-torsorial (λ y → B x ≃ B y)
is-torsorial-fam-equiv-is-univalent {x} =
fundamental-theorem-id' (λ y → equiv-tr B) (U x)

dependent-universal-property-identity-system-fam-equiv-is-univalent :
{x : A} →
dependent-universal-property-identity-system (λ y → B x ≃ B y) id-equiv
dependent-universal-property-identity-system-fam-equiv-is-univalent {x} =
dependent-universal-property-identity-system-is-torsorial
( id-equiv)
( is-torsorial-fam-equiv-is-univalent {x})


### Inclusions of subuniverses into the universe are univalent

Note. This proof relies on essential use of the univalence axiom.

module _
{l1 l2 : Level} (S : subuniverse l1 l2)
where

is-univalent-inclusion-subuniverse : is-univalent (inclusion-subuniverse S)
is-univalent-inclusion-subuniverse =
is-univalent-is-emb (is-emb-inclusion-subuniverse S)