# Tooling to make copies of lattice structures #

Sometimes it is useful to make a copy of a lattice structure where one replaces the data parts with provably equal definitions that have better definitional properties.

def OrderTop.copy {α : Type u} {h : LE α} {h' : LE α} (c : ) (top : α) (eq_top : top = ) (le_eq : ∀ (x y : α), x y x y) :

A function to create a provable equal copy of a top order with possibly different definitional equalities.

Equations
• c.copy top eq_top le_eq =
Instances For
def OrderBot.copy {α : Type u} {h : LE α} {h' : LE α} (c : ) (bot : α) (eq_bot : bot = ) (le_eq : ∀ (x y : α), x y x y) :

A function to create a provable equal copy of a bottom order with possibly different definitional equalities.

Equations
• c.copy bot eq_bot le_eq =
Instances For
def BoundedOrder.copy {α : Type u} {h : LE α} {h' : LE α} (c : ) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (le_eq : ∀ (x y : α), x y x y) :

A function to create a provable equal copy of a bounded order with possibly different definitional equalities.

Equations
• c.copy top eq_top bot eq_bot le_eq = BoundedOrder.mk
Instances For
def Lattice.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) :

A function to create a provable equal copy of a lattice with possibly different definitional equalities.

Equations
• c.copy le eq_le sup eq_sup inf eq_inf = Lattice.mk
Instances For
def DistribLattice.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) :

A function to create a provable equal copy of a distributive lattice with possibly different definitional equalities.

Equations
• c.copy le eq_le sup eq_sup inf eq_inf =
Instances For
def GeneralizedHeytingAlgebra.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (himp : ααα) (eq_himp : himp = HImp.himp) :

A function to create a provable equal copy of a generalised heyting algebra with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top sup eq_sup inf eq_inf himp eq_himp =
Instances For
def GeneralizedCoheytingAlgebra.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) :

A function to create a provable equal copy of a generalised coheyting algebra with possibly different definitional equalities.

Equations
• c.copy le eq_le bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff =
Instances For
def HeytingAlgebra.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) :

A function to create a provable equal copy of a heyting algebra with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl =
Instances For
def CoheytingAlgebra.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) :

A function to create a provable equal copy of a coheyting algebra with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot =
Instances For
def BiheytingAlgebra.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) :

A function to create a provable equal copy of a biheyting algebra with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot himp eq_himp compl eq_compl =
Instances For
def CompleteLattice.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

A function to create a provable equal copy of a complete lattice with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf = CompleteLattice.mk
Instances For
def Frame.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

A function to create a provable equal copy of a frame with possibly different definitional equalities.

Equations
• Frame.copy c le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf himp eq_himp compl eq_compl sSup eq_sSup sInf eq_sInf =
Instances For
def Coframe.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

A function to create a provable equal copy of a coframe with possibly different definitional equalities.

Equations
• Coframe.copy c le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot sSup eq_sSup sInf eq_sInf =
Instances For
def CompleteDistribLattice.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (top : α) (eq_top : top = ) (bot : α) (eq_bot : bot = ) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sdiff : ααα) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : αα) (eq_hnot : hnot = HNot.hnot) (himp : ααα) (eq_himp : himp = HImp.himp) (compl : αα) (eq_compl : compl = HasCompl.compl) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

A function to create a provable equal copy of a complete distributive lattice with possibly different definitional equalities.

Equations
• c.copy le eq_le top eq_top bot eq_bot sup eq_sup inf eq_inf sdiff eq_sdiff hnot eq_hnot himp eq_himp compl eq_compl sSup eq_sSup sInf eq_sInf =
Instances For
def ConditionallyCompleteLattice.copy {α : Type u} (c : ) (le : ααProp) (eq_le : le = LE.le) (sup : ααα) (eq_sup : sup = Sup.sup) (inf : ααα) (eq_inf : inf = Inf.inf) (sSup : Set αα) (eq_sSup : sSup = SupSet.sSup) (sInf : Set αα) (eq_sInf : sInf = InfSet.sInf) :

A function to create a provable equal copy of a conditionally complete lattice with possibly different definitional equalities.

Equations
• c.copy le eq_le sup eq_sup inf eq_inf sSup eq_sSup sInf eq_sInf =
Instances For