Definition make_latticeob {L : C} {meet_mor join_mor : C⟦L ⊗ L,L⟧} : latticeop_cat meet_mor join_mor → latticeob L := λ (isL : latticeop_cat meet_mor join_mor), meet_mor,, join_mor ,, isL.
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.