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.
A function to create a provable equal copy of a lattice with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a distributive lattice with possibly different definitional equalities.
Instances For
A function to create a provable equal copy of a generalised heyting algebra with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a generalised coheyting algebra with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a heyting algebra with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a coheyting algebra with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a biheyting algebra with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a complete lattice with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a frame with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a coframe with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a complete distributive lattice with possibly different definitional equalities.
Equations
Instances For
A function to create a provable equal copy of a conditionally complete lattice with possibly different definitional equalities.