Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.Require ImportRequire Import HoTT.Classes.interfaces.abstract_algebra. Instance join_bool : Join Bool := orb. Instance meet_bool : Meet Bool := andb. Instance bottom_bool : Bottom Bool := false. Instance top_bool : Top Bool := true. Section contents. Local Ltac solve_bool := repeat (intros [|]); compute; (contradiction || auto). #[export] Instance lattice_bool : IsBoundedLattice Bool.IsBoundedLattice Bool Proof.IsBoundedLattice Bool repeat split; (apply _ || solve_bool). Defined. End contents.