---

Step * of Lemma sets-id

∀[C:SmallCategory]. ∀[X:Top].  (cat-id(sets(C; X)) ~ λA.(cat-id(C) (fst(A))))
BY
{ ((Auto THEN (Assert C ∈ SmallCategory BY Trivial))
   THEN DCat 1
   THEN RepUR ``sets presheaf-elements mk-cat I_set`` 0
   THEN RWO "op-cat-id" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:Top].    (cat-id(sets(C;  X))  \msim{}  \mlambda{}A.(cat-id(C)  (fst(A))))


By

---

Latex:
((Auto  THEN  (Assert  C  \mmember{}  SmallCategory  BY  Trivial))
  THEN  DCat  1
  THEN  RepUR  ``sets  presheaf-elements  mk-cat  I\_set``  0
  THEN  RWO  "op-cat-id"  0
  THEN  Auto)

---

Home Index