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