Dependent types I › Universes, or types of types
14 days ago
- #type-theory
- #dependent-types
- #universes
- Dependent type theory involves two main entities: types and their elements.
- Universes are types whose elements are themselves types, enabling polymorphic functions and type-level operations.
- A universe is defined as a type with a family closed under type constructors, addressing syntactic and semantic objections.
- The axiom of universes ensures universes exist for any finite sequence of families, allowing hierarchical universe structures.
- Large elimination or a universe is required to prove non-triviality of booleans (e.g., true ≠ false).
- Identification types provide a way to witness sameness between elements, with rules for formation, introduction, elimination, and computation.
- Structural rules in type theory ensure judgmental equality behaves correctly, including reflexivity, transitivity, and symmetry.
- Implicit definitions in type theory rely on the uniqueness of functions satisfying given equations, contrasting with explicit definitions.
- Pasting and flipping operations on identifications allow combining and reversing witnesses of sameness, with properties like associativity and inversion.
- Exercises include proving properties of identification types, universe hierarchies, and the non-triviality of booleans.