# Contents

## Idea

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.

## References

Observational type theory was introduced in

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)