Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Just a note: both “propositional type theory” and “weak type theory” are synonyms of “objective type theory” in this subfield. See e.g. van der Berg’s slides at the DutchCATS conference on weak type theory:
Propositional type theory is a version of type theory without definitional equality and in which all computation rules are stated in propositional form. (Other names: homotopy type theory with explicit conversions or objective type theory.)
Or Spadetto’s slides from the same conference:
Objective/propositional/weak type theory
In:
Benno van den Berg, Martijn den Besten, Quadratic type checking for objective type theory, 2021.
All the existing literature, starting from Winterhalter’s paper and continuing to the present day, imply that “weak type theory” does not have any definitional equality / conversions / judgmental equality, and this includes conversion of types to defined aliases. Even explicit substitution uses identity types instead of judgmental equality.
So this article should be merged into objective type theory.
renamed page to be about any type theory with propositional computation rules, and moved stuff about weak type theory over to objective type theory
Actually, changed my mind. The authors never really address the issue of definitions in the literature. The thing is that “propositional type theory” is overloaded as a term: in van der Berg, judgmental equality is α-equivalence and definitions are made with identity types, but in Spadetto, the dependent type theory comes with judgmental definitional equality.
1 to 6 of 6