Re:Relation Between Type Theory, Category Theory and Logic
by igravious on Saturday July 11, 2015 @05:59AM
(#9869224)
When you think about it we do have a computational meaning and interpretation for the univalence axiom. Your very comment was such an exposition!
What we perhaps don't have is an automated implementation of your exposition. What you're talking about is typecasting where all the terms of one type map to all the terms of another type. And that once shown this the machine could perform type substitution kind of like how type inference works now. (And maybe the machine wouldn't always have to be shown??) Neat idea. Automatic type inference is pretty powerful. Automatic type substitution could be just as powerful perhaps.
What we perhaps don't have is an automated implementation of your exposition. What you're talking about is typecasting where all the terms of one type map to all the terms of another type. And that once shown this the machine could perform type substitution kind of like how type inference works now. (And maybe the machine wouldn't always have to be shown??) Neat idea. Automatic type inference is pretty powerful. Automatic type substitution could be just as powerful perhaps.