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)
identity type, equivalence of types, definitional isomorphism
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
In dependent type theory, given a type , the autoequivalence type of is the equivalence type between and itself, . The elements (terms) of are called autoequivalences or self-equivalences.
is an -group.
Given a univalent Russell universe and an element , there is an equivalence between and the loop space type , . is called the automorphism -group in at .
The autoequivalence type on an -truncated type is an -group.
If is a set, then is the symmetric group on and is also written as , , or , and the elements of are called permutations. Every autoequivalence type is a symmetric group in a dependent type theory with axiom K or uniqueness of identity proofs.
If is a mere proposition, then is a contractible type.
Given types and , there is a function .
Given an infinity-group , the delooping of is defined to be a higher inductive type generated by equivalences and , and identity
loop space type (for the equivalent for identity types)
Last revised on July 6, 2024 at 10:04:44. See the history of this page for a list of all contributions to it.