Showing changes from revision #0 to #1:
Added | Removed | Changed
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.