Extensionality of lambda-*
Logic in Computer Science
2014-01-07 v1
Abstract
We prove an extensionality theorem for the "type-in-type" dependent type theory with Sigma-types. We suggest that the extensional equality type be identified with the logical equivalence relation on the free term model of type theory.
Keywords
Cite
@article{arxiv.1401.1139,
title = {Extensionality of lambda-*},
author = {Andrew Polonsky},
journal= {arXiv preprint arXiv:1401.1139},
year = {2014}
}
Comments
25 pages