Definition latticeop_cat {L} (meet_mor join_mor : C⟦L ⊗ L,L⟧) := (isassoc_cat meet_mor × iscomm_cat meet_mor) × (isassoc_cat join_mor × iscomm_cat join_mor) × (isabsorb_cat meet_mor join_mor × isabsorb_cat join_mor meet_mor).
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.