Step
*
1
3
1
2
of Lemma
presheaf-elements_wf
.....wf..... 
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
5. A2 : cat-ob(op-cat(C))
6. B1 : P A2
⊢ istype({f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} )
BY
{ (D 0 THEN Auto) }
Latex:
Latex:
.....wf..... 
1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  A  :  cat-ob(op-cat(C))
4.  A1  :  P  A
5.  A2  :  cat-ob(op-cat(C))
6.  B1  :  P  A2
\mvdash{}  istype(\{f:cat-arrow(op-cat(C))  A2  A|  (P  A2  A  f  B1)  =  A1\}  )
By
Latex:
(D  0  THEN  Auto)
Home
Index