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 : OrderTop α) (top : α) (eq_top : top = ⊤) (le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y) : OrderTop α

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 = OrderTop.mk ⋯

def OrderBot.copy {α : Type u} {h : LE α} {h' : LE α} (c : OrderBot α) (bot : α) (eq_bot : bot = ⊥) (le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y) : OrderBot α

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 = OrderBot.mk ⋯

def BoundedOrder.copy {α : Type u} {h : LE α} {h' : LE α} (c : BoundedOrder α) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y) : BoundedOrder α

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

def Lattice.copy {α : Type u} (c : Lattice α) (le : α → α → Prop) (eq_le : le = LE.le) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) : Lattice α

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 inf ⋯ ⋯ ⋯

def DistribLattice.copy {α : Type u} (c : DistribLattice α) (le : α → α → Prop) (eq_le : le = LE.le) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) : DistribLattice α

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 = DistribLattice.mk ⋯

def GeneralizedHeytingAlgebra.copy {α : Type u} (c : GeneralizedHeytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α) (eq_himp : himp = HImp.himp) : GeneralizedHeytingAlgebra α

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 = GeneralizedHeytingAlgebra.mk ⋯

def GeneralizedCoheytingAlgebra.copy {α : Type u} (c : GeneralizedCoheytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sdiff : α → α → α) (eq_sdiff : sdiff = SDiff.sdiff) : GeneralizedCoheytingAlgebra α

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 = GeneralizedCoheytingAlgebra.mk ⋯

def HeytingAlgebra.copy {α : Type u} (c : HeytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = HasCompl.compl) : HeytingAlgebra α

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 = HeytingAlgebra.mk ⋯

def CoheytingAlgebra.copy {α : Type u} (c : CoheytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sdiff : α → α → α) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : α → α) (eq_hnot : hnot = HNot.hnot) : CoheytingAlgebra α

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 = CoheytingAlgebra.mk ⋯

def BiheytingAlgebra.copy {α : Type u} (c : BiheytingAlgebra α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sdiff : α → α → α) (eq_sdiff : sdiff = SDiff.sdiff) (hnot : α → α) (eq_hnot : hnot = HNot.hnot) (himp : α → α → α) (eq_himp : himp = HImp.himp) (compl : α → α) (eq_compl : compl = HasCompl.compl) : BiheytingAlgebra α

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 = BiheytingAlgebra.mk ⋯ ⋯

def CompleteLattice.copy {α : Type u} (c : CompleteLattice α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sSup : Set α → α) (eq_sSup : sSup = SupSet.sSup) (sInf : Set α → α) (eq_sInf : sInf = InfSet.sInf) : CompleteLattice α

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 ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

def Frame.copy {α : Type u} (c : Order.Frame α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (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) : Order.Frame α

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 = Order.Frame.mk ⋯ ⋯ ⋯

def Coframe.copy {α : Type u} (c : Order.Coframe α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (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) : Order.Coframe α

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 = Order.Coframe.mk ⋯ ⋯ ⋯

def CompleteDistribLattice.copy {α : Type u} (c : CompleteDistribLattice α) (le : α → α → Prop) (eq_le : le = LE.le) (top : α) (eq_top : top = ⊤) (bot : α) (eq_bot : bot = ⊥) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (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) : CompleteDistribLattice α

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 = CompleteDistribLattice.mk ⋯ ⋯ ⋯

def ConditionallyCompleteLattice.copy {α : Type u} (c : ConditionallyCompleteLattice α) (le : α → α → Prop) (eq_le : le = LE.le) (sup : α → α → α) (eq_sup : sup = max) (inf : α → α → α) (eq_inf : inf = min) (sSup : Set α → α) (eq_sSup : sSup = SupSet.sSup) (sInf : Set α → α) (eq_sInf : sInf = InfSet.sInf) : ConditionallyCompleteLattice α

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 = ConditionallyCompleteLattice.mk ⋯ ⋯ ⋯ ⋯