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
What is called observational type theory (OTT) is a flavor of type theory in between extensional type theory and intensional type theory.
This may be regarded as a first-stage approximation to homotopy type theory (HoTT, and for more motivation see at higher observational type theory):
The propositions of OTT correspond to the h-propositions of HoTT, and the types in OTT correspond to h-sets in HoTT. The notion of equality on OTT is based on symmetric prosets, which is a special case of higher internal groupoids. Since equality is defined type-by-type, OTT enjoys function extensionality, and a form of propositional extensionality at least for a specified universe of propositions (not necessarily including all h-propositions).
There are a few technical differences (e.g. proofs of propositions are definitionally equal in OTT, whereas proofs of hprops are only propositionally equal in HoTT) but on the whole HoTT looks a lot like a higher homotopy version of OTT.
Observational type theory was introduced in:
Thorsten Altenkirch, Conor McBride, Towards observational type theory, draft (2006) [pdf, pdf, pdf]
Thorsten Altenkirch, Conor McBride, Wouter Swierstra, Observational Equality, Now!, PLPV ‘07: Proceedings of the 2007 workshop on Programming languages meets program verification (2007) 57-68 [ISBN:978-1-59593-677-6, doi:10.1145/1292597.1292608, pdf]
A blog post about an Agda implementation, including propositional extensionality (which is not mentioned in ABS07):
The above comparison between OTT and HoTT is taken from
Last revised on January 3, 2024 at 00:26:40. See the history of this page for a list of all contributions to it.