I've been working on a little side-project called Fine to explore some of the foundations of type theory. I haven't had much time recently to pursue it, so I'm writing up the work I've already done. A preliminary implementation is on GitHub, or you can look at the rudimentary language tutorial using RawGit. Function intensionality The main goal of Fine is to explore what a world without function extensionality would be like. I've written before that basic type theories usually leave open the ...
