3 ms·
Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?
by lakecresva 6y ago
Can you give a practical example of how denying UIP helps with tasks like writing a proof or a definition rather than defining a really exotic inductive type?