Post #2061448
2026-04-18 23:12 UTC
@ncf this feels... extremely unintuitive. like, there's no data to go off! everything's truncated! (assuming the type that's being related in a set, i guess)
how can you ever construct anything that's not a proposition out of this?
Replies (1)
-
@ncf@types.pl 2026-04-18 23:15
@mei Being a decidable order is a proposition (if you don't know why, then... sub-puzzle!), so you can remove the truncation in "strong total order" when proving this.