Showing changes from revision #4 to #5:
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:
Revision on October 11, 2018 at 12:59:46 by Ali Caglayan. See the history of this page for a list of all contributions to it.