nLab impredicative polymorphism

 Definition

For universes

A type universe $U$ has impredicative polymorphism or is impredicative if dependent product types of $U$-indexed families of $U$-small types are themselves $U$-small.

For Russell universes, this is given by the inference rule

$$\frac{\Gamma, X:U \vdash P(X):U}{\Gamma \vdash \prod_{X:U} P(X):U}$$

The situation is a little bit more complicated for Tarski universes. Like all other conditions on Tarski universes, there is an orthogonal axis for which impredicativity might vary: weak or strict impredicativity, which has to do with whether one uses an equivalence of types or judgmental equality to define small types.

• A Tarski universe $(U, T)$ has weak impredicative polymorphism or is weakly impredicative if for all functions $P:U \to U$ the dependent product type $\prod_{X:U} P(X)$ is essentially $U$-small

$$\prod_{P:U \to U} \sum_{\forall_P:U} T(\forall_P) \simeq \prod_{X:U} T(P(X))$$

• A Tarski universe $(U, T)$ has strict impredicative polymorphism or is strictly impredicative if for all functions $P:U \to U$ the dependent product type $\prod_{X:U} P(X)$ is $U$-small

$$\frac{\Gamma, X:U \vdash P(X):U}{\Gamma \vdash \forall X:U.P(X):U} \qquad \frac{\Gamma, X:U \vdash P(X):U}{\Gamma \vdash T(\forall X:U.P(X)) \equiv \prod_{X:U} T(P(X)) \; \mathrm{type}}$$

For dependent type theories

In the presentation of dependent type theory using a hierarchy of universes, impredicative polymorphism is a resizing axiom which says that for all endofunctions $P:U_0 \to U_0$ on the first type universe $U_0$, the dependent product type $\prod_{X:U_0} P(X)$ is (essentially) $U_0$-small.

In dependent type theory with type variables, presented without universes but with a single type judgment, while there is no universe $U_0$ to quantify over for the dependent product type, using the type variable we can add an untyped version of the dependent product type $\Pi X.P(X)$ to the type theory for impredicative polymorphism. This type is similar to universal quantification $\forall X.P(X)$ in untyped first-order logic, and $\Pi X.P(X)$ plays the same role in this presentation of dependent type theory that the type $\prod_{X:U_0} P(X)$ does for the other presentation of dependnet type theory. The rules for $\Pi X.P(X)$ are as follows:

Formation rule:

$$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type}}{\Gamma \vdash \Pi X.P(X) \; \mathrm{type}}$$

Introduction rule:

$$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma, X \; \mathrm{type} \vdash p(X):P(x)}{\Gamma \vdash \lambda X.p(X):\Pi X.P(X)}$$

Elimination rule:

$$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma \vdash p:\Pi X.P(X)}{\Gamma, A \; \mathrm{type} \vdash \mathrm{ev}(p, X):P(X)}$$

Computation rules:

• Judgmental computation rule:
  $$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma, X \; \mathrm{type} \vdash p(X):P(x)}{\Gamma, X \; \mathrm{type} \vdash \mathrm{ev}(\lambda X.p(X), X) \equiv p(X):P(X)}$$
• Typal computation rule:
  $$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma, X \; \mathrm{type} \vdash p(X):P(x)}{\Gamma, X \; \mathrm{type} \vdash \beta_\Pi^{P, p}(X):\mathrm{ev}(\lambda X.p(X), X) =_{P(X)} p(X)}$$

Uniqueness rules:

• Judgmental uniqueness rule:
  $$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma \vdash p:\Pi X.P(X)}{\Gamma \vdash \lambda X.\mathrm{ev}(p, X) \equiv p:\Pi X.P(x)}$$
• Typal uniqueness rule:
  $$\frac{\Gamma, X \; \mathrm{type} \vdash P(X) \; \mathrm{type} \quad \Gamma \vdash p:\Pi X.P(X)}{\Gamma \vdash \eta_\Pi^P(p):\lambda X.\mathrm{ev}(p, X) =_{\Pi X.P(x)} p}$$

 Examples of universes with impredicative polymorphism

• The base universe $\mathrm{Set}$ historically had impredicative polymorphism in Coq, according to Pédrot 2022.

• In dependent type theory defined using a single type judgment, the universe of all propositions is a type universe with impredicative polymorphism if and only if weak function extensionality holds.

• More generally, let $\Omega$ be a universe of propositions, and assume weak function extensionality holds. Then $\Omega$ has impredicative polymorphism if and only if it is closed under dependent product types of predicates in $\Omega$; i.e. $\Omega$ is an inflattice.

 Related concepts

• polymorphism

• internal parametricity

• impredicative universe

• impredicative dependent type theory

• propositional resizing

• taboo

• type of all propositions

• weak function extensionality

• dependent type theory with type variables

 References

• Andrew Pitts, Nontrivial Power Types can’t be Subtypes of Polymorphic Types (pdf)

• Taichi Uemura, Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing, in 24th International Conference on Types for Proofs and Programs (TYPES 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 130, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) (doi:10.4230/LIPIcs.TYPES.2018.7, arXiv:1803.06649)

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

• Pierre-Marie Pédrot, Why not have Prop : Set in Coq?, Proof Assistant StackExchange, 27 June 2022. (web)

• Mere propositions and Consistency with Impredicativity, Excluded Middle and Large Elimination, Proof Assistant StackExchange (web)