@jdw I guess this is related to "Dickson's lemma" which has an intuitionistic proof according to [1], with the caveat that [1] talks about infinite sequences rather than well-founded induction.
According to [2, Corollary 2.4], you can show that an ordering R is well-founded by showing that in the classifying topos of "an infinite R-decreasing chain", false holds. This *should* close the gap between your question and the claim in [1], but there is surely a more direct answer. There's quite a lot of literature on this type of "constructive Ramsey theory".
[1] W. Veldman, An intuitionistic proof of Kruskal’s theorem
[2] https://www.speicherleck.de/iblech/stuff/early-draft-modal-multiverse.pdf
David Wärn
@dwarn@mathstodon.xyz
mastodon
4.5.8
PhD student in homotopy type theory at the University of Gothenburg
0
Followers
0
Following
Joined December 12, 2022
Posts
David Wärn
@dwarn@mathstodon.xyz
PhD student in homotopy type theory at the University of Gothenburg
mathstodon.xyz
David Wärn
@dwarn@mathstodon.xyz
PhD student in homotopy type theory at the University of Gothenburg
mathstodon.xyz
@dwarn@mathstodon.xyz
·
Mar 23, 2026
2
2
0
David Wärn
@dwarn@mathstodon.xyz
PhD student in homotopy type theory at the University of Gothenburg
mathstodon.xyz
David Wärn
@dwarn@mathstodon.xyz
PhD student in homotopy type theory at the University of Gothenburg
mathstodon.xyz
@dwarn@mathstodon.xyz
·
Feb 18, 2026
A HoTT exercise: let \( A \) be a type with a binary operation \( * : A \to A \to A \). Suppose that \( * \) is associative, commutative, and idempotent, in the sense that \( \Pi_{a\, b\, c : A} a * (b * c) = (a * b) * c \), \( \Pi_{a\, b : A} a * b = b * a \) and \( \Pi_{a : A} a * a = a \). Show that \( A \) is an hset (and hence a semilattice in the ordinary sense).
25
0
9