Commit 2026-09-15 17:41 73c2c934

View on Github →

chore(Order/CompleteLattice/Basic): Sort* polymorphism (#39857) Generalize some theorems from Type* to Sort*. Also make type-variables explicitly either Type* or Sort*.

Estimated changes

modified theorem iSup_comp_le
modified theorem iSup_iSup_eq_left
modified theorem iSup_iSup_eq_right
modified theorem iSup_image
modified theorem iSup_of_empty'
modified theorem iSup_psigma'
modified theorem iSup_psigma
modified theorem iSup_split
modified theorem iSup_split_single
modified theorem iSup_subtype''