|
|
|
|
|
|
by nyrikki
26 days ago
|
|
|
The Curry-Howard correspondence formal relationship between intuitionistic logic and typed lambda calculus. Intuitionistic logic doesn’t hold PEM as a priori. Due to many issues like [0] you actually lose the univalent in HoTT. That is what allows you to say two programs are equivalent by behavior. No comment on the OP, but be careful as it is a rabbit hole. [0] https://ncatlab.org/nlab/show/Diaconescu-Goodman-Myhill+theo... |
|
|