---

Step * of Lemma sets-arrow

∀[C:SmallCategory]. ∀[X:Top].
  (cat-arrow(sets(C; X)) ~ λAa,Bb. let A,a = Aa in let B,b = Bb in {f:cat-arrow(C) A B| f(b) = a ∈ (X A)} )
BY
{ ((Auto THEN (Assert C ∈ SmallCategory BY Trivial))
   THEN DCat 1
   THEN RepUR ``sets presheaf-elements mk-cat I_set psc-restriction`` 0
   THEN RWO "op-cat-arrow" 0
   THEN Auto
   THEN Computation) }

---

Latex:

---

Latex:
\mforall{}[C:SmallCategory].  \mforall{}[X:Top].
    (cat-arrow(sets(C;  X))  \msim{}  \mlambda{}Aa,Bb.  let  A,a  =  Aa  in  let  B,b  =  Bb  in  \{f:cat-arrow(C)  A  B|  f(b)  =  a\}  )


By

---

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

---

Home Index