Complete lattice redundant parameter

Stream: general

[Kenny Lau]

Isn't bot and top provable from supremum and infimum, respectively?

[Mario Carneiro]

Yes, and Sup is definable from Inf, and sup is definable from Sup. The reason these additional definitions are in the structure is that sometimes you want a different definitional reduction for the expression than the lattice definition gives you, i.e. Prop is a complete lattice with top true, but if it was defined with Sup then that would be some cumbersome forall false thing