 |
Post AvlUEPDnRq29pqCWW0 by [email protected] |
 |
More posts by [email protected] |
|
Post #AvlUEP0gEbXfBA434S by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jeanas @ncf I am sure you can translate this Agda proof by induction on natura… |
|
|
|
Post #AvlUEP7PpYvhW3DQZM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @jeanas No, since positive-not-zero uses universes. |
|
|
|
Post #AvlUEPDnRq29pqCWW0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf @jeanas OK, you win! |
|
|
|
Post #AvlUEPJp5Qr28X1KuO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf What survives from my argument is the following.(1) If 0=1, then equality … |
|
|
|
Post #AvlUEPQuf4WeUWKzxY by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @ncf ~~We can model this in a preorder.~~ (EDIT: misread the pos… |
|
|
|
Post #AvlUEPXIHLd6oJK5uC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jonmsterling @MartinEscardo Wouldn't a preorder have 0 = 1? |
|
|
|
Post #AvlUEPdJuwRz708uIa by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf @MartinEscardo Sorry, I totally misread Martin's comment. |
|
|
|
Post #AvlUEVmP45HUAuRFI0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
It's known that 0 ≠ 1 is independent from MLTT without universes. Can the… |
|
|
|
Post #AvlUEVt8f2fWVnacmu by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf The identity type 0=0 in the natural numbers is contractible, because it i… |
|
|
|
Post #AvlUEVyoJxConOF9d2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo The natural numbers don't have decidable equality without un… |
|
|
|
Post #AvlUEW5BwEJH7BEFZg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf They do! |
|
|
|
Post #AvlUEWSaXF1cHkAw2i by [email protected] |
|
0 likes, 0 repeats |
|
|
|
I wrote: "They do".To add more, you don't need to know that 0 ≠… |
|
|
|
Post #AvlUEpW7gK8rOCyWgq by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo MLTT has canonicity, right? So to prove 0 = 1 or 0 ≠ 1 you rea… |
|
|
|
Post #AvlUEpc9JuxjgtnL5E by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf No. In all models in which 0=1, everything is equal. |
|
|
|
Post #AvlUEvM3ydezUkJZqK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo OK, maybe I should split my question into two:Is it provable in … |
|
|
|
Post #AvlUEvT9YHKbqjdEtU by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ncf @MartinEscardo Here is a proof that ℕ is a set by a Hedberg-style argume… |
|
|
|
Post #AvlUEvab6bHoDp7BUu by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@ecavallo @ncf @MartinEscardo this is amazing… |
