natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
In type theory what is called the UIP axiom, the axiom of uniqueness of identity proofs is an axiom that when added to intensional type theory turns it into a propositionally extensional type theory.
The axiom asserts that any two terms of the same identity type are themselves propositionally equal (in the corresponding higher identity type).
This is contrary to the univalence axiom, which makes sense only in the absence of UIP.
The UIP axiom (for types in a universe “”) posits that the type
has a term. In other words, we add to our type theory the rule
We can modify this by making the hypotheses of the axiom into premises of the rule, if we wish. In particular, this can be used to give a version of the rule that applies to all types not necessarily belonging to some fixed universe, using the judgment “” for “ is a type” (as distinguished from “” for “ belongs to the universe type ”).
Discussion in Coq is in
Last revised on August 9, 2018 at 17:39:26. See the history of this page for a list of all contributions to it.