The parametricity axiom

Content created by Fredrik Bakke.

Created on 2026-03-06.
Last modified on 2026-03-06.

module foundation.parametricity-axiom where
Imports 
open import foundation.parametric-types
open import foundation.universe-levels

Idea

The parametricity axiom states that all types are parametric at their own universe level. I.e., for each type X : 𝒰, the constant map

  X → (𝒰 → X)

is an equivalence.

Jem Lord [Lor25] presents this as internal parametricity. Since we only work internally to type theory internal parametricity is all we can reason about, so we dub it simply parametricity. Many consequences of parametricity are also explored in [BELS17].

Definition

level-Parametricity : (l : Level) → UU (lsuc l)
level-Parametricity l = {X : UU l} → is-parametric l X

Parametricity : UUω
Parametricity = {l : Level} → level-Parametricity l

References

[BELS17]
Auke Bart Booij, Martín Hötzel Escardó, Peter LeFanu Lumsdaine, and Michael Shulman. Parametricity, automorphisms of the universe, and excluded middle. 2017. arXiv:1701.05617.
[Lor25]
Jem Lord. Easy parametricity. 2025. URL: https://hott-uf.github.io/2025/abstracts/HoTTUF\%5F2025\%5Fpaper\%5F21.pdf.

Recent changes