Definition sub_bounded_latticeob : bounded_latticeob BPC TC M. Proof. use make_bounded_latticeob. - exact (sub_latticeob BPC Hi l Hmeet Hjoin). - exact bot_mor_M. - exact top_mor_M. - split. + now apply (islunit_cat_comm Hjoin Hbot), (islunit_join_mor_bot_mor BPC TC l). + now apply (islunit_cat_comm Hmeet Htop), (islunit_meet_mor_top_mor BPC TC l). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal.