Constructive order theory puzzle! Prove that every strong total order is decidable (and conversely every decidable total order is strong), with the following definitions:
A partial order is a binary relation that is reflexive, transitive and antisymmetric.A total order is a partial order in which ∀ x y. ∥ (x ≤ y) + (y ≤ x) ∥.A strong total order is a partial order in which ∥ ∀ x y. (x ≤ y) + (y ≤ x) ∥ (hence a total order).An order is decidable if ∀ x y. (x ≤ y) + ¬(x ≤ y).
Naïm Camille Favier
@ncf@types.pl
mastodon
4.6.0-alpha.5+glitch
PhD student at Chalmers interested in univalent foundations, category theory and music.
0
Followers
0
Following
Joined May 25, 2023
web:
Posts
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
2d ago
16
0
5
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Apr 13, 2026
0
0
0
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Apr 09, 2026
IMAGINE, IF YOU WILL, A PERSON WHO HAS BUILT HIS IDENTITY AND CAREER ON HIS LOVE AND KNOWLEDGE OF LOGIC; WHO HAS SPENT YEARS AND CONSIDERABLE MONEY STUDYING LOGIC; WHO HAS GRADUATED WITH A DEGREE IN LOGIC; WHO PERHAPS TEACHES LOGIC TO CHILDREN OR EVEN LECTURES ON IT AT A UNIVERSITY. NOW IMAGINE DISCOVERING THAT THIS PERSON HAS ONLY EVER HEARD ABOUT ONE FOUNDATION IN THEIR ENTIRE LIFE: IT IS THE ZERMELO–FRAENKEL SET THEORY.
13
0
2
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Apr 01, 2026
@jcreed at least yes assuming Whitehead's principle, since A₀ is n-connected for all n.
1
0
0
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Mar 31, 2026
I've just added to my formalisation of @jemlord 's "Easy Parametricity" a short proof that every function of type (A : U) → A → A is the identity. Such a neat idea!
17
0
4
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Mar 20, 2026
@ionchy anyway good post
1
0
0
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Mar 20, 2026
2
4
0
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Mar 20, 2026
@wilbowma I think this is a useful post and I mostly agree with your conclusions, although I am not a fan of the structure.
I think you phrased every argument except your own in a way that is very easy to refute by making them about the technology (and not the AI industry), only presenting their "real" versions in the section about power. But this is what (most) people really mean by these arguments, and I think it sounds a bit disingenuous to pretend otherwise.
I also have other complaints that were already raised here, but overall thank you for writing this.
I think you phrased every argument except your own in a way that is very easy to refute by making them about the technology (and not the AI industry), only presenting their "real" versions in the section about power. But this is what (most) people really mean by these arguments, and I think it sounds a bit disingenuous to pretend otherwise.
I also have other complaints that were already raised here, but overall thank you for writing this.
1
0
1
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Oct 15, 2025
@zwarich that's the most citation-needed [citation needed] that's ever needed citation
0
2
0
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
Naïm Camille Favier
@ncf@types.pl
PhD student at Chalmers interested in univalent foundations, category theory and music.
types.pl
@ncf@types.pl
·
Oct 15, 2025
2
0
0