---

Step * 1 1 of Lemma presheaf-elements_wf

.....subterm..... T:t
3:n
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. Aa : A:cat-ob(op-cat(C)) × (P A)
⊢ cat-id(op-cat(C)) (fst(Aa)) ∈ let A,a = Aa 
                                in let B,b = Aa 
                                   in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} 
BY
{ (D -1 THEN Reduce 0) }

1
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)} 

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  Aa  :  A:cat-ob(op-cat(C))  \mtimes{}  (P  A)
\mvdash{}  cat-id(op-cat(C))  (fst(Aa))  \mmember{}  let  A,a  =  Aa 
                                                                in  let  B,b  =  Aa 
                                                                      in  \{f:cat-arrow(op-cat(C))  B  A|  (P  B  A  f  b)  =  a\} 


By

---

Latex:
(D  -1  THEN  Reduce  0)

---

Home Index