Timeline for Cannot discriminate `0 = 1`
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 19, 2022 at 11:14 | vote | accept | Tempestas Ludi | ||
| Apr 15, 2022 at 13:50 | answer | added | HTNW | timeline score: 6 | |
| Apr 15, 2022 at 13:27 | history | edited | Guy Coder |
edited tags
|
|
| Apr 15, 2022 at 8:50 | comment | added | Tempestas Ludi |
Oh, I see now that there are solutions. These solve the entire exercise by exact (λ p, transportf (nat_rect (λ _, UU) unit (λ _ _, empty)) p tt). It will take some time to unpack that, but at least I have a solution now.
|
|
| Apr 14, 2022 at 22:22 | comment | added | Mike Shulman |
I don't know anything about UniMath in particular, but I believe discriminate is not designed univalently, so it may not work. I don't know what the authors of those exercises recommended, but the standard way to prove this "by hand" is a simplified version of the encode-decode method.
|
|
| Apr 14, 2022 at 0:33 | comment | added | Tempestas Ludi |
intros contra. discriminate. gives the same result
|
|
| Apr 13, 2022 at 14:30 | history | edited | Guy Coder |
edited tags
|
|
| Apr 13, 2022 at 14:13 | comment | added | Agnishom Chattopadhyay |
Have you tried just discriminate?
|
|
| S Apr 13, 2022 at 12:11 | review | First questions | |||
| Apr 13, 2022 at 13:39 | |||||
| S Apr 13, 2022 at 12:11 | history | asked | Tempestas Ludi | CC BY-SA 4.0 |