---

Step * of Lemma free-dist-lattice-property

No Annotations
∀T:Type. ∀eq:EqDecider(T). ∀L:BoundedDistributiveLattice. ∀eqL:EqDecider(Point(L)). ∀f:T ⟶ Point(L).
  ∃g:Hom(free-dist-lattice(T; eq);L). (f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L)))
BY
{ (Auto
   THEN With
   ⌜λac.lattice-extend(L;eq;eqL;f;ac)⌝ (D 0)⋅
   THEN Auto
   THEN Try ((FunExt THEN RepUR ``compose`` 0 THEN Auto))) }

1
.....wf..... 
1. T : Type@i'
2. eq : EqDecider(T)@i
3. L : BoundedDistributiveLattice@i'
4. eqL : EqDecider(Point(L))@i
5. f : T ⟶ Point(L)@i
⊢ λac.lattice-extend(L;eq;eqL;f;ac) ∈ Hom(free-dist-lattice(T; eq);L)

---

Latex:

---

Latex:
No  Annotations
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:BoundedDistributiveLattice.  \mforall{}eqL:EqDecider(Point(L)).
\mforall{}f:T  {}\mrightarrow{}  Point(L).
    \mexists{}g:Hom(free-dist-lattice(T;  eq);L).  (f  =  (g  o  (\mlambda{}x.free-dl-inc(x))))


By

---

Latex:
(Auto
  THEN  With
  \mkleeneopen{}\mlambda{}ac.lattice-extend(L;eq;eqL;f;ac)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Try  ((FunExt  THEN  RepUR  ``compose``  0  THEN  Auto)))

---

Home Index