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
equality (definitional, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
basic constructions:
strong axioms
further
Just as there are two notions of judgmental equality in dependent type theory, judgmental equality of terms and judgmental equality of types, there are two types in dependent type theory which could be considered typal equality:
In type universes $U$, this means that small types $A:U$ have two notions of typal equality, one from the identity type between small types, and the other from the equivalence type between small types, and the univalence axiom states that these two types are equivalent (i.e. typally equal) to each other.
The parallels between the structural rules for judgmental equality and typal equality are shown below:
judgmental equality | typal equality |
---|---|
judgmental equality of terms | identification |
reflexivity of judgmental equality of terms | identity identification |
symmetry of judgmental equality of terms | inverse identification |
transitivity of judgmental equality of terms | composition of identifications |
judgmental equality of types | equivalence |
reflexivity of judgmental equality of types | identity equivalence |
symmetry of judgmental equality of types | inverse equivalence |
transitivity of judgmental equality of types | composition of equivalences |
principle of substitution | transport |
variable conversion rule | substitution of evaluation of inverse equivalence |
homogeneous identification | heterogeneous identification | homogeneous equivalence | heterogeneous equivalence | |
---|---|---|---|---|
type | $a =_A b$ | $x =_B^p y$ | $A \simeq B$ | $A \simeq B$ |
identity term | $\mathrm{refl}_A(a):a =_A a$ | $\mathrm{apd}_B^p(f):f(a) =_B^p f(b)$ | $\mathrm{id}_A:A \simeq A$ | $\mathrm{tr}_B^p:B(a) \simeq B(b)$ |
Last revised on January 19, 2023 at 23:13:27. See the history of this page for a list of all contributions to it.