---

Step * of Lemma cube-cat-final

Final({})
BY
{ (RepUR ``cat-final cube-cat names-hom`` 0 THEN Auto) }

1
1. x : fset(ℕ)
2. f : names({}) ⟶ Point(dM(x))
3. g : names({}) ⟶ Point(dM(x))
⊢ f = g ∈ (names({}) ⟶ Point(dM(x)))

2
1. [x] : fset(ℕ)
2. ∀[f,g:names({}) ⟶ Point(dM(x))].  (f = g ∈ (names({}) ⟶ Point(dM(x))))
3. names({})
⊢ Point(dM(x))

---

Latex:

---

Latex:
Final(\{\})


By

---

Latex:
(RepUR  ``cat-final  cube-cat  names-hom``  0  THEN  Auto)

---

Home Index