nLab equivalence induction

Idea

In dependent type theory, equivalence induction says that equivalence types are inductively generated by the identity equivalence, in the same way that identity types are inductively generated by reflexivity. Like the induction principle of identity types, there are two versions of equvialence induction, the standard (Martin-Lof style) equivalence induction and the based (Paulin-Mohrung style) equivalence induction.

Equivalence induction is equivalent in strength to the univalence axiom, because equivalence induction makes the equivalence type behave like an identity system, which then makes the equivalence type equivalent to the identity type between types, which is precisely the univalence axiom. Conversely, corollary 5.8.5 of the HoTT Book derives equivalence induction from the univalence axiom.

Definition

Using universes

Equivalence induction is usually formulated using universes $U$, such as in Corollary 5.8.5 of the HoTT Book.

Definition

The (based Paulin-Mohrung style) equivalence induction states that given $U$-small types $A:U$ and a $U$-small type family $P(X, e)$ indexed by $U$-small type $X:U$ and equivalence $e:A \simeq X$, and an element $T:P(A, \mathrm{idequiv}_A)$, for all $X:U$ and $e:A \simeq X$ one can construct an element $\mathrm{ind}_\simeq^P(T, X, e):P(X, e)$ such that $T = \mathrm{ind}_\simeq^P(T, A, \mathrm{idequiv}_A)$.

The inference rules for this version of equivalence induction are given by:

$$\frac{\Gamma \vdash A:U \quad \Gamma, X:U, e:A \simeq X \vdash P(X, e):U}{\Gamma, T:P(A, \mathrm{idequiv}_A), X:U, e:A \simeq X \vdash P(X, e) \vdash \mathrm{ind}_\simeq^P(T, X, e):P(X, e)}$$

$$\frac{\Gamma \vdash A:U \quad \Gamma, X:U, e:A \simeq X \vdash P(X, e):U}{\Gamma, T:P(A, \mathrm{idequiv}_A) \vdash \mathrm{ind}_\simeq^P(T, A, \mathrm{idequiv}_A) \equiv T:P(A, \mathrm{idequiv}_A)}$$

Definition

The (standard Martin-Lof style) equivalence induction states that given a $U$-small type family $P(X, Y, e)$ indexed by $U$-small types $X:U$ and $Y:U$ and equivalence $e:X \simeq Y$, and a dependent function $T:\prod_{A:U} P(A, A, \mathrm{idequiv}_A)$, for all $X:U$, $Y:U$, and $e:X \simeq Y$ one can construct an element $\mathrm{ind}_\simeq^P(T, X, Y, e):P(X, Y, e)$ such that $T(X) = \mathrm{ind}_\simeq^P(T, X, X, \mathrm{idequiv}_X)$.

The inference rules for this version of equivalence induction are given by:

$$\frac{\Gamma, X:U, Y:U, e:X \simeq Y \vdash P(X, Y, e):U}{\Gamma, T:\prod_{A:U} P(A, A, \mathrm{idequiv}_A), X:U, Y:U, e:X \simeq Y \vdash P(X, Y, e) \vdash \mathrm{ind}_\simeq^P(T, X, Y, e):P(X, Y, e)}$$

$$\frac{\Gamma, X:U, Y:U, e:X \simeq Y \vdash P(X, Y, e):U}{\Gamma, T:\prod_{A:U} P(A, A, \mathrm{idequiv}_A), X:U \vdash \mathrm{ind}_\simeq^P(T, X, X, \mathrm{idequiv}_X) \equiv T(X):P(X, X, \mathrm{idequiv}_X)}$$

Using type variables

Traditionally, equivalence induction is formulated using universes, such as in Corollary 5.8.5 of the HoTT Book. However, with type variables, one can express equivalence induction without using universes.

Definition

The (based Paulin-Mohrung style) equivalence induction states that given type $A$ and a type family $P(X, e)$ indexed by type $X$ and equivalence $e:A \simeq X$, and an element $T:P(A, \mathrm{idequiv}_A)$, for all types $X$ and $e:A \simeq X$ one can construct an element $\mathrm{ind}_\simeq^P(T, X, e):P(X, e)$ such that $T = \mathrm{ind}_\simeq^P(T, A, \mathrm{idequiv}_A)$.

The inference rules for this version of equivalence induction are given by:

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, X \; \mathrm{type}, e:A \simeq X \vdash P(X, e) \; \mathrm{type}}{\Gamma, T:P(A, \mathrm{idequiv}_A), X \; \mathrm{type}, e:A \simeq X \vdash P(X, e) \vdash \mathrm{ind}_\simeq^P(T, X, e):P(X, e)}$$

$$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, X \; \mathrm{type}, e:A \simeq X \vdash P(X, e) \; \mathrm{type}}{\Gamma, T:P(A, \mathrm{idequiv}_A) \vdash \mathrm{ind}_\simeq^P(T, A, \mathrm{idequiv}_A) \equiv T:P(A, \mathrm{idequiv}_A)}$$

With type variables and impredicative polymorphism, one can also express the standard equivalence induction without using universes.

Definition

The (standard Martin-Lof style) equivalence induction states that given a type family $P(X, Y, e)$ indexed by types $X$ and $Y$ and equivalence $e:X \simeq Y$, and an element $T:\Pi A.P(A, A, \mathrm{idequiv}_A)$, for all types $X$, $Y$, and equivalences $e:X \simeq Y$ one can construct an element $\mathrm{ind}_\simeq^P(T, X, Y, e):P(X, Y, e)$ such that $T(X) = \mathrm{ind}_\simeq^P(T, X, X, \mathrm{idequiv}_X)$.

The inference rules for this version of equivalence induction are given by:

$$\frac{\Gamma, X \; \mathrm{type}, Y \; \mathrm{type}, e:X \simeq Y \vdash P(X, Y, e) \; \mathrm{type}}{\Gamma, T:\forall A.P(A, A, \mathrm{idequiv}_A), X \; \mathrm{type}, Y \; \mathrm{type}, e:X \simeq Y \vdash P(X, Y, e) \vdash \mathrm{ind}_\simeq^P(T, X, Y, e):P(X, Y, e)}$$

$$\frac{\Gamma, X \; \mathrm{type}, Y \; \mathrm{type}, e:X \simeq Y \vdash P(X, Y, e) \; \mathrm{type}}{\Gamma, T:\forall A.P(A, A, \mathrm{idequiv}_A), X \; \mathrm{type} \vdash \mathrm{ind}_\simeq^P(T, X, X, \mathrm{idequiv}_X) \equiv T(X):P(X, X, \mathrm{idequiv}_X)}$$

In cubical type theory

In cubical type theory with glue types and either type universes or type variables, equivalence induction is provable from the glue types. This is in contrast with the usual Martin-Lof type theory where equivalence induction is a set of two unjustified inference rules equivalent in strength to the univalence axiom.

Related concepts

• equivalence of types

• equivalence type

• identity type

• univalence axiom

References

Equivalence induction is defined using universes in corollary 5.8.5 of:

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)

Equivalence induction is defined using type variables in:

• Dependent Type Theory vs Polymorphic Type Theory, Category Theory Zulip (web)