---

Step * 1 1 1 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
⊢ cat-id(op-cat(C)) A ∈ {f:cat-arrow(op-cat(C)) A A| (P A A f A1) = A1 ∈ (P A)} 
BY
{ (At ⌜Type⌝ MemTypeCD⋅ THEN Auto) }

1
.....set predicate..... 
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A : cat-ob(op-cat(C))
4. A1 : P A
⊢ (P A A (cat-id(op-cat(C)) A) A1) = A1 ∈ (P A)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  A  :  cat-ob(op-cat(C))
4.  A1  :  P  A
\mvdash{}  cat-id(op-cat(C))  A  \mmember{}  \{f:cat-arrow(op-cat(C))  A  A|  (P  A  A  f  A1)  =  A1\} 


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Auto)

---

Home Index