- lo.logic type-systems coq normalization agda
- Updated Wed, 22 Jun 2022 05:30:06 GMT

In particular Agda seems not strong enough to prove that.

Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?

How about with the impredicative Prop?

Coq without Prop is not strong enough, because it's basically Martin-Lf type theory with universes.

Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.

- +0 – Is there an existing Coq formalization? — Jun 08, 2018 at 16:37
- +1 – @ukaszLew I couldn't find anything compelling online, but there is a Lego formalization by Altenkirch (1993!) described here: cs.nott.ac.uk/~psztxa/publ/tlca93.pdf — Jun 08, 2018 at 19:12
- +1 – Found two more: Strong normalization for System F by HOAS on top of FOAS and Girard Normalization Proof in LEGO, page 67 — Jun 09, 2018 at 00:49
- +0 – Here's one in Coq! github.com/coq-community/autosubst/blob/master/examples/ssr/… — Jun 09, 2022 at 18:46

Local articles referenced by this article: