---

Step * of Lemma presheaf-elements-sq

∀C:SmallCategory. ∀P:Top.
  (el(P) ~ Cat(ob = A:cat-ob(C) × (ob(P) A);
               arrow(Aa,Bb) = let A,a = Aa 
                              in let B,b = Bb 
                                 in {f:cat-arrow(op-cat(C)) B A| (arrow(P) B A f b) = a ∈ (ob(P) A)} ;
               id(Aa) = cat-id(C) (fst(Aa));
               comp(Aa,Bb,Dd,f,g) = cat-comp(C) (fst(Aa)) (fst(Bb)) (fst(Dd)) f g))
BY
{ (Auto THEN RepeatFor 2 (D 1) THEN DProdsAndUnions THEN (Auto THEN RepUR ``presheaf-elements op-cat`` 0) THEN SqEqCD) }

---

Latex:

---

Latex:
\mforall{}C:SmallCategory.  \mforall{}P:Top.
    (el(P)  \msim{}  Cat(ob  =  A:cat-ob(C)  \mtimes{}  (ob(P)  A);
                              arrow(Aa,Bb)  =  let  A,a  =  Aa 
                                                            in  let  B,b  =  Bb 
                                                                  in  \{f:cat-arrow(op-cat(C))  B  A|  (arrow(P)  B  A  f  b)  =  a\}  ;
                              id(Aa)  =  cat-id(C)  (fst(Aa));
                              comp(Aa,Bb,Dd,f,g)  =  cat-comp(C)  (fst(Aa))  (fst(Bb))  (fst(Dd))  f  g))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  1)
  THEN  DProdsAndUnions
  THEN  (Auto  THEN  RepUR  ``presheaf-elements  op-cat``  0)
  THEN  SqEqCD)

---

Home Index