[TYPES] Implementing induction principles

Thomas Streicher streicher at mathematik.tu-darmstadt.de
Tue Jun 23 07:44:20 EDT 2009


That induction over N does not imply uniqueness (i.e. eta fails for R)
is shown on pp.101-102 of my Habilitation Thesis (1993) available at

 www.mathematik.tu-darmstadt.de/~streicher/HabilStreicher.pdf

Thomas 


More information about the Types-list mailing list