---

Step * of Lemma forget-lattice_wf

ForgetLattice ∈ Functor(BddDistributiveLattice;TypeCat)
BY
{ (Unfold `forget-lattice` 0
   THEN MemCD
   THEN Try (QuickAuto)
   THEN All (RepUR  ``type-cat distributive-lattice-cat mk-cat``)
   THEN Auto) }

---

Latex:

---

Latex:
ForgetLattice  \mmember{}  Functor(BddDistributiveLattice;TypeCat)


By

---

Latex:
(Unfold  `forget-lattice`  0
  THEN  MemCD
  THEN  Try  (QuickAuto)
  THEN  All  (RepUR    ``type-cat  distributive-lattice-cat  mk-cat``)
  THEN  Auto)

---

Home Index