Definition sub_latticeob : latticeob BPC M. Proof. use make_latticeob. - apply meet_mor_M. - apply join_mor_M. - repeat split. + now apply (isassoc_cat_comm Hmeet), (isassoc_meet_mor _ l). + now apply (iscomm_cat_comm Hmeet), (iscomm_meet_mor _ l). + now apply (isassoc_cat_comm Hjoin), (isassoc_join_mor _ l). + now apply (iscomm_cat_comm Hjoin), (iscomm_join_mor _ l). + now apply (isabsorb_cat_comm Hmeet Hjoin), (meet_mor_absorb_join_mor _ l). + now apply (isabsorb_cat_comm Hjoin Hmeet), (join_mor_absorb_meet_mor _ 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.