---

Step * 1 1 2 1 1 of Lemma free-DeMorgan-algebra-property


1. T : Type@i'
2. eq : EqDecider(T)@i
3. dm : DeMorganAlgebra@i'
4. eq2 : EqDecider(Point(dm))@i
5. f : T ⟶ Point(dm)@i
6. g : Hom(free-DeMorgan-lattice(T;eq);dm)
7. (λp.case p of inl(a) => f a | inr(a) => ¬(f a)) = (g o (λx.free-dl-inc(x))) ∈ ((T + T) ⟶ Point(dm))
8. ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
9. ∀i:T. ((g <1-i>) = ¬(f i) ∈ Point(dm))
⊢ ∀[a:Point(free-DeMorgan-lattice(T;eq))]. ((g a) = ¬(g ¬(a)) ∈ Point(dm))
BY
{ ((InstLemma `free-dist-lattice-hom-unique` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜dm⌝;⌜eq2⌝;⌜λp.case p
                                                                                             of inl(a) =>
                                                                                             f a
                                                                                             | inr(a) =>
                                                                                             ¬(f a)⌝]⋅
    THENA Auto
    )
   THEN Fold `free-DeMorgan-lattice` (-1)
   THEN (InstHyp [⌜g⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. dm : DeMorganAlgebra@i'
4. eq2 : EqDecider(Point(dm))@i
5. f : T ⟶ Point(dm)@i
6. g : Hom(free-DeMorgan-lattice(T;eq);dm)
7. (λp.case p of inl(a) => f a | inr(a) => ¬(f a)) = (g o (λx.free-dl-inc(x))) ∈ ((T + T) ⟶ Point(dm))
8. ∀i:T. ((g <i>) = (f i) ∈ Point(dm))
9. ∀i:T. ((g <1-i>) = ¬(f i) ∈ Point(dm))
10. ∀h:Hom(free-DeMorgan-lattice(T;eq);dm)
      (((λp.case p of inl(a) => f a | inr(a) => ¬(f a)) = (g o (λx.free-dl-inc(x))) ∈ ((T + T) ⟶ Point(dm)))
      ⇒ ((λp.case p of inl(a) => f a | inr(a) => ¬(f a)) = (h o (λx.free-dl-inc(x))) ∈ ((T + T) ⟶ Point(dm)))
      ⇒ (g = h ∈ Hom(free-DeMorgan-lattice(T;eq);dm)))
⊢ ∀[a:Point(free-DeMorgan-lattice(T;eq))]. ((g a) = ¬(g ¬(a)) ∈ Point(dm))

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  dm  :  DeMorganAlgebra@i'
4.  eq2  :  EqDecider(Point(dm))@i
5.  f  :  T  {}\mrightarrow{}  Point(dm)@i
6.  g  :  Hom(free-DeMorgan-lattice(T;eq);dm)
7.  (\mlambda{}p.case  p  of  inl(a)  =>  f  a  |  inr(a)  =>  \mneg{}(f  a))  =  (g  o  (\mlambda{}x.free-dl-inc(x)))
8.  \mforall{}i:T.  ((g  <i>)  =  (f  i))
9.  \mforall{}i:T.  ((g  ə-i>)  =  \mneg{}(f  i))
\mvdash{}  \mforall{}[a:Point(free-DeMorgan-lattice(T;eq))].  ((g  a)  =  \mneg{}(g  \mneg{}(a)))


By

---

Latex:
((InstLemma  `free-dist-lattice-hom-unique`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};\mkleeneopen{}dm\mkleeneclose{};\mkleeneopen{}eq2\mkleeneclose{};
    \mkleeneopen{}\mlambda{}p.case  p  of  inl(a)  =>  f  a  |  inr(a)  =>  \mneg{}(f  a)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Fold  `free-DeMorgan-lattice`  (-1)
  THEN  (InstHyp  [\mkleeneopen{}g\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2))

---

Home Index