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 set-level type theory.
The axiom asserts that any two terms of the same identity type $Id_A(x,y)$ 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 “$Type$”) 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 “$A\;type$” for “$A$ is a type” (as distinguished from “$A:Type$” for “$A$ belongs to the universe type $Type$”).
There is also a definitional version of UIP, where any two terms of the same identity type or path type are definitionally equal. It is given by the following rule:
Definitional UIP is implied by boundary separation in cubical type theory.
Discussion in Coq is in
For definitional UIP in XTT
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).
Last revised on September 3, 2022 at 12:05:25. See the history of this page for a list of all contributions to it.