Identity Types
a day ago
- #Type Theory
- #Dependent Types
- #Category Theory
- Deep connection between mathematics and programming, with programs dealing with mathematical objects like numbers, vectors, etc.
- Definition of natural numbers in Haskell and the problem of encoding laws they obey using equalities.
- Two types of equality: definitional (part of the definition) and propositional (requires proof).
- In type theory, equality is a type (identity type), representing proofs of equality, and is a dependent type.
- Introduction rule for identity type: reflexivity constructor (refl) generates a witness for equality.
- Identity elimination rule (path induction): defines a function from a path to some type, using a dependent function.
- Categorical model of identity types: modeled as a fibration, with introduction and elimination rules interpreted categorically.
- Path induction's uniqueness and agreement with reflexivity, illustrated via commuting diagrams.
- Connection to homotopy theory hinted at, with identity types having non-trivial inhabitants called paths.