The category of finite bounded distributive lattices #
This file defines
FinBddDistLat, the category of finite distributive lattices with
bounded lattice homomorphisms.
- FinBddDistLat.instDistribLatticeαToDistLatToBddDistLat X = X.toBddDistLat.toDistLat.str
Constructs an equivalence between finite distributive lattices from an order isomorphism between them.
- One or more equations did not get rendered due to their size.