This page is under construction. - Ali
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: * for any , an element
Revision on September 6, 2018 at 11:46:12 by Ali Caglayan. See the history of this page for a list of all contributions to it.