# Library HoTT.Metatheory.Core

# Metatheory

Definition Funext_type@{i j max} :=

∀ (A : Type@{i}) (P : A → Type@{j}) f g,

IsEquiv (@apD10@{i j max} A P f g).

Univalence is a property of a single universe; its statement lives in a higher universe

Definition Univalence_type@{i iplusone} : Type@{iplusone} :=

∀ (A B : Type@{i}), IsEquiv (equiv_path@{i i iplusone i} A B).

∀ (A B : Type@{i}), IsEquiv (equiv_path@{i i iplusone i} A B).