Showing changes from revision #10 to #11:
Added | Removed | Changed
The identity type has elements that are witnesses to the βsamenessβ of elements.
The identity type can be defined as the inductive type? with the following constructor:
Identity types have the following formation rule
Univalent Foundations Project, Homotopy Type Theory β Univalent Foundations of Mathematics (2013)
Mike Shulman, Towards a Third-Generation HOTT Part 1 (slides, video)