 |
Posts by [email protected] |
 |
Post #AvlUE3h7U8Px4PkdAO by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jonmsterling @carloangiuli @danielgratzer Would some kind of descent condition… |
|
|
|
Post #AvlUE4mpQOZuSPQhhg by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jonmsterling @carloangiuli @danielgratzer And, out of curiosity, what would a … |
|
|
|
Post #AvlUEP7PpYvhW3DQZM by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo @jeanas No, since positive-not-zero uses universes. |
|
|
|
Post #AvlUEPXIHLd6oJK5uC by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@jonmsterling @MartinEscardo Wouldn't a preorder have 0 = 1? |
|
|
|
Post #AvlUEVmP45HUAuRFI0 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
It's known that 0 ≠ 1 is independent from MLTT without universes. Can the… |
|
|
|
Post #AvlUEVyoJxConOF9d2 by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo The natural numbers don't have decidable equality without un… |
|
|
|
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 #AvlUEvM3ydezUkJZqK by [email protected] |
|
0 likes, 0 repeats |
|
|
|
@MartinEscardo OK, maybe I should split my question into two:Is it provable in … |
|
|
|
Post #AxOw8CsoW3QWsGv9UW by [email protected] |
|
0 likes, 0 repeats |
|
|
|
do you really need choice to extract a 2-cocycle from a central extension |
