---

Step * of Lemma dm-neg-is-hom

∀[T:Type]. ∀[eq:EqDecider(T)].
  (λx.¬(x) ∈ Hom(free-DeMorgan-lattice(T;eq);opposite-lattice(free-DeMorgan-lattice(T;eq))))
BY
{ (Auto
   THEN Unfold `dm-neg` 0
   THEN (Assert Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq))) BY
               (RW (SubC (SymbCompC [`free-DeMorgan-lattice`] 30)) 0 THEN Auto))
   THEN (Assert deq-fset(deq-fset(union-deq(T;T;eq;eq)))
                ∈ EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))) BY
               (RevHypSubst 3 0 THEN Unfold `free-DeMorgan-lattice` 0 THEN RWO "free-dl-point" 0 THEN Auto))
   THEN (InstLemma `lattice-extend-is-hom` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;
         ⌜opposite-lattice(free-DeMorgan-lattice(T;eq))⌝;⌜deq-fset(deq-fset(union-deq(T;T;eq;eq)))⌝]⋅
         THENA Auto
         )
   THEN BHyp -1 
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
4. deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
5. ∀[f:(T + T) ⟶ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))]
     (λac.lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
                         deq-fset(deq-fset(union-deq(T;T;eq;eq)));f;ac)
      ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));opposite-lattice(free-DeMorgan-lattice(T;eq))))
6. x : T@i
⊢ {{inr x }} ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))

2
1. T : Type
2. eq : EqDecider(T)
3. Point(free-DeMorgan-lattice(T;eq)) ~ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))
4. deq-fset(deq-fset(union-deq(T;T;eq;eq))) ∈ EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))
5. ∀[f:(T + T) ⟶ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))]
     (λac.lattice-extend(opposite-lattice(free-DeMorgan-lattice(T;eq));union-deq(T;T;eq;eq);
                         deq-fset(deq-fset(union-deq(T;T;eq;eq)));f;ac)
      ∈ Hom(free-dist-lattice(T + T; union-deq(T;T;eq;eq));opposite-lattice(free-DeMorgan-lattice(T;eq))))
6. y : T@i
⊢ {{inl y}} ∈ Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].
    (\mlambda{}x.\mneg{}(x)  \mmember{}  Hom(free-DeMorgan-lattice(T;eq);opposite-lattice(free-DeMorgan-lattice(T;eq))))


By

---

Latex:
(Auto
  THEN  Unfold  `dm-neg`  0
  THEN  (Assert  Point(free-DeMorgan-lattice(T;eq)) 
                          \msim{}  Point(opposite-lattice(free-DeMorgan-lattice(T;eq)))  BY
                          (RW  (SubC  (SymbCompC  [`free-DeMorgan-lattice`]  30))  0  THEN  Auto))
  THEN  (Assert  deq-fset(deq-fset(union-deq(T;T;eq;eq)))
                            \mmember{}  EqDecider(Point(opposite-lattice(free-DeMorgan-lattice(T;eq))))  BY
                          (RevHypSubst  3  0
                            THEN  Unfold  `free-DeMorgan-lattice`  0
                            THEN  RWO  "free-dl-point"  0
                            THEN  Auto))
  THEN  (InstLemma  `lattice-extend-is-hom`  [\mkleeneopen{}T  +  T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};
              \mkleeneopen{}opposite-lattice(free-DeMorgan-lattice(T;eq))\mkleeneclose{};\mkleeneopen{}deq-fset(deq-fset(union-deq(T;T;eq;eq)))\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  BHyp  -1 
  THEN  Auto)

---

Home Index