fact: Definition make_bounded_latticeob {L} {l : latticeob L} {bot top : C⟦TC,L⟧} : bounded_latticeop_cat l bot top → bounded_latticeob L := λ bl, l,, bot,, top,, bl.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Terminal