Step
*
3
1
1
1
1
of Lemma
free-dist-lattice-adjunction
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. d : Type
4. x : d
5. (fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x))
= free-dl-generator(free-dl-generator(x))
∈ Point(free-dl(Point(free-dl(d))))
⊢ (fdl-hom(free-dl(d);λg.g)
(fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x)))
= free-dl-generator(x)
∈ Point(free-dl(d))
BY
{ (ApFunToHypEquands `Z' ⌜fdl-hom(free-dl(d);λg.g) Z⌝ ⌜Point(free-dl(d))⌝ (-1)⋅ THENA 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. d : Type
4. x : d
5. (fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x))
= free-dl-generator(free-dl-generator(x))
∈ Point(free-dl(Point(free-dl(d))))
6. (fdl-hom(free-dl(d);λg.g)
(fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x)))
= (fdl-hom(free-dl(d);λg.g) free-dl-generator(free-dl-generator(x)))
∈ Point(free-dl(d))
⊢ (fdl-hom(free-dl(d);λg.g)
(fdl-hom(free-dl(Point(free-dl(d)));λx.free-dl-generator(free-dl-generator(x))) free-dl-generator(x)))
= free-dl-generator(x)
∈ Point(free-dl(d))
Latex:
Latex:
1. \mforall{}Y:Type. (Point(free-dl(Y)) \msim{} free-dl-type(Y))
2. \mforall{}Y:Type. \mforall{}y:Y. (free-dl-generator(y) \mmember{} Point(free-dl(Y)))
3. d : Type
4. x : d
5. (fdl-hom(free-dl(Point(free-dl(d)));\mlambda{}x.free-dl-generator(free-dl-generator(x)))
free-dl-generator(x))
= free-dl-generator(free-dl-generator(x))
\mvdash{} (fdl-hom(free-dl(d);\mlambda{}g.g)
(fdl-hom(free-dl(Point(free-dl(d)));\mlambda{}x.free-dl-generator(free-dl-generator(x)))
free-dl-generator(x)))
= free-dl-generator(x)
By
Latex:
(ApFunToHypEquands `Z' \mkleeneopen{}fdl-hom(free-dl(d);\mlambda{}g.g) Z\mkleeneclose{} \mkleeneopen{}Point(free-dl(d))\mkleeneclose{} (-1)\mcdot{} THENA Auto)
Home
Index