2014/01/06 by Andrew Polonsky, Polonsky, Andrew
Computer Science · #03F50 #F.4.1 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #acm:03F50 #cs.LO #msc:03F50
paper · pdf · doi:10.48550/arxiv.1401.1139
25 pages
arxiv created 2014/01/06 · arxiv updated 2014/01/07
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.