## Idea ## Higher observational type theory involves a different definition of [[identity types]] where the identity types are defined recursively for each type former rather than uniformly across all types. ## See also ## * [[homotopy type theory]] ## References ## * Mike Shulman, Towards a Third-Generation HOTT Part 1 ([slides](https://www.cmu.edu/dietrich/philosophy/hott/slides/shulman-2022-04-28.pdf), [video](https://www.youtube.com/watch?v=FrxkVzItMzA))