fact: Definition default_join_sl_le `{IsJoinSemiLattice L} : Le L := fun x y => x ⊔ y = y.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.orders.semirings HoTT.Classes.theory.lattices