observational type theory

**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.

It may be regarded as a first-stage approximation to homotopy type theory (HoTT): 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 setoids, which is a special case of higher internal groupoids. 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-dimensional version of OTT.

Observational type theory was introduced in

- Thorsten Altenkirch and Conor McBride,
*Towards observational type theory*(pdf)

The above comparison between OTT and HoTT is taken from

Revised on November 30, 2012 02:05:44
by Toby Bartels
(64.89.53.239)