---

Step * of Lemma free-dl-functor_wf

FreeDistLattice ∈ Functor(TypeCat;BddDistributiveLattice)
BY
{ (((Assert ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y)) BY
           (Intro THEN RW (SubC (TagC (mk_tag_term 100))) 0 THEN Auto))
    THEN (Assert ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y))) BY
                (ParallelOp 1 THEN RWO  "-1" 0 THEN Auto))
    )
   THEN ProveWfLemma
   THEN All (RepUR  ``type-cat distributive-lattice-cat mk-cat``)
   THEN Auto
   THEN (BLemma `free-dl-generators` THEN Auto)
   THEN Try ((BLemma `id-is-bounded-lattice-hom` THEN Auto))
   THEN Try ((Using [`l2',⌜free-dl(Y)⌝] (BLemma `compose-bounded-lattice-hom`)⋅ THEN Auto))) }

1
1. ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y))
2. ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y)))
3. X : Type
4. Y : Type
5. z : Type
6. f : X ⟶ Y
7. g : Y ⟶ z
8. x : X
⊢ (fdl-hom(free-dl(z);λx@0.free-dl-generator(g (f x@0))) free-dl-generator(x))
= ((fdl-hom(free-dl(z);λx.free-dl-generator(g x)) o fdl-hom(free-dl(Y);λx.free-dl-generator(f x))) free-dl-generator(x))
∈ Point(free-dl(z))

2
1. ∀Y:Type. (Point(free-dl(Y)) ~ free-dl-type(Y))
2. ∀Y:Type. ∀y:Y.  (free-dl-generator(y) ∈ Point(free-dl(Y)))
3. X : Type
4. x : X
⊢ (fdl-hom(free-dl(X);λx@0.free-dl-generator(x@0)) free-dl-generator(x))
= ((λx.x) free-dl-generator(x))
∈ Point(free-dl(X))

---

Latex:

---

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


By

---

Latex:
(((Assert  \mforall{}Y:Type.  (Point(free-dl(Y))  \msim{}  free-dl-type(Y))  BY
                  (Intro  THEN  RW  (SubC  (TagC  (mk\_tag\_term  100)))  0  THEN  Auto))
    THEN  (Assert  \mforall{}Y:Type.  \mforall{}y:Y.    (free-dl-generator(y)  \mmember{}  Point(free-dl(Y)))  BY
                            (ParallelOp  1  THEN  RWO    "-1"  0  THEN  Auto))
    )
  THEN  ProveWfLemma
  THEN  All  (RepUR    ``type-cat  distributive-lattice-cat  mk-cat``)
  THEN  Auto
  THEN  (BLemma  `free-dl-generators`  THEN  Auto)
  THEN  Try  ((BLemma  `id-is-bounded-lattice-hom`  THEN  Auto))
  THEN  Try  ((Using  [`l2',\mkleeneopen{}free-dl(Y)\mkleeneclose{}]  (BLemma  `compose-bounded-lattice-hom`)\mcdot{}  THEN  Auto)))

---

Home Index