6 ms·
> it has canonicity, which I'd argue is necessary for a general-purpose programming language MLTT, even without HoTT/CTT, already features canonicity, no? (At
by curryhoward 6y ago
> it has canonicity, which I'd argue is necessary for a general-purpose programming language
MLTT, even without HoTT/CTT, already features canonicity, no? (At least for positive types.)
I thought the main advantage of HoTT is that you can define non-trivial equalities, and the advantage of CTT in particular is that univalence can be derived in it (rather than introducing it as a non-computational axiom).
- remexre 6y agoRight, I think I'd put univalence in my list of "I want this for my dream general-purpose dependently-typed programming language" features; being able to prove properties on simple representations of data and transport those properties to more optimized forms is pretty important, imo.