---

Step * 1 of Lemma free-dist-lattice-hom-unique


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
6. g : Hom(free-dist-lattice(T; eq);L)@i
7. h : Hom(free-dist-lattice(T; eq);L)@i
8. f = (g o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L))@i
9. f = (h o (λx.free-dl-inc(x))) ∈ (T ⟶ Point(L))@i
10. x : T@i
⊢ (g free-dl-inc(x)) = (h free-dl-inc(x)) ∈ Point(L)
BY
{ (RepeatFor 2 (((ApFunToHypEquands `Z' ⌜Z x⌝ ⌜Point(L)⌝ (-3)⋅ THENA Auto) THEN Reduce (-1))) THEN Eq) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  L  :  BoundedDistributiveLattice@i'
4.  eqL  :  EqDecider(Point(L))@i
5.  f  :  T  {}\mrightarrow{}  Point(L)@i
6.  g  :  Hom(free-dist-lattice(T;  eq);L)@i
7.  h  :  Hom(free-dist-lattice(T;  eq);L)@i
8.  f  =  (g  o  (\mlambda{}x.free-dl-inc(x)))@i
9.  f  =  (h  o  (\mlambda{}x.free-dl-inc(x)))@i
10.  x  :  T@i
\mvdash{}  (g  free-dl-inc(x))  =  (h  free-dl-inc(x))


By

---

Latex:
(RepeatFor  2  (((ApFunToHypEquands  `Z'  \mkleeneopen{}Z  x\mkleeneclose{}  \mkleeneopen{}Point(L)\mkleeneclose{}  (-3)\mcdot{}  THENA  Auto)  THEN  Reduce  (-1)))  THEN  Eq)

---

Home Index