---

Step * of Lemma dm-neg-is-hom-opposite

∀[T:Type]. ∀[eq:EqDecider(T)].
  (λx.¬(x) ∈ Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq)))
BY
{ (Auto THEN MemTypeCD) }

1
1. T : Type
2. eq : EqDecider(T)
⊢ λx.¬(x) ∈ Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq))

2
.....set predicate..... 
1. T : Type
2. eq : EqDecider(T)
⊢ (((λx.¬(x)) 0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ (((λx.¬(x)) 1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))

3
.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. f : Hom(opposite-lattice(free-DeMorgan-lattice(T;eq));free-DeMorgan-lattice(T;eq))
⊢ ((f 0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ ((f 1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq))) ∈ Type

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  MemTypeCD)

---

Home Index