---

Step * 1 of Lemma presheaf-elements_wf


1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ el(P) ∈ SmallCategory
BY
{ ((Unfold `presheaf-elements` 0 THEN At ⌜Type⌝MemCD⋅) THEN Try (QuickAuto)) }

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

2
.....subterm..... T:t
4:n
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. Aa : A:cat-ob(op-cat(C)) × (P A)
4. Bb : A:cat-ob(op-cat(C)) × (P A)
5. Dd : A:cat-ob(op-cat(C)) × (P A)
6. f : let A,a = Aa 
       in let B,b = Bb 
          in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} 
7. g : let A,a = Bb 
       in let B,b = Dd 
          in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} 
⊢ cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) g f ∈ let A,a = Aa 
                                                          in let B,b = Dd 
                                                             in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} 

3
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ ∀Aa,Bb:A:cat-ob(op-cat(C)) × (P A). ∀f:let A,a = Aa 
                                         in let B,b = Bb 
                                            in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} .
    (((cat-comp(op-cat(C)) (fst(Bb)) (fst(Aa)) (fst(Aa)) f (cat-id(op-cat(C)) (fst(Aa))))
    = f
    ∈ let A,a = Aa 
      in let B,b = Bb 
         in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} )
    ∧ ((cat-comp(op-cat(C)) (fst(Bb)) (fst(Bb)) (fst(Aa)) (cat-id(op-cat(C)) (fst(Bb))) f)
      = f
      ∈ let A,a = Aa 
        in let B,b = Bb 
           in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} ))

4
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
⊢ ∀Aa,Bb,z,Dd:A:cat-ob(op-cat(C)) × (P A). ∀f:let A,a = Aa 
                                              in let B,b = Bb 
                                                 in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} .
  ∀g:let A,a = Bb 
     in let B,b = z 
        in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} . ∀h:let A,a = z 
                                                                     in let B,b = Dd 
                                                                        in {f:cat-arrow(op-cat(C)) B A| 
                                                                            (P B A f b) = a ∈ (P A)} .
    ((cat-comp(op-cat(C)) (fst(Dd)) (fst(z)) (fst(Aa)) h (cat-comp(op-cat(C)) (fst(z)) (fst(Bb)) (fst(Aa)) g f))
    = (cat-comp(op-cat(C)) (fst(Dd)) (fst(Bb)) (fst(Aa)) (cat-comp(op-cat(C)) (fst(Dd)) (fst(z)) (fst(Bb)) h g) f)
    ∈ let A,a = Aa 
      in let B,b = Dd 
         in {f:cat-arrow(op-cat(C)) B A| (P B A f b) = a ∈ (P A)} )

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
\mvdash{}  el(P)  \mmember{}  SmallCategory


By

---

Latex:
((Unfold  `presheaf-elements`  0  THEN  At  \mkleeneopen{}Type\mkleeneclose{}MemCD\mcdot{})  THEN  Try  (QuickAuto))

---

Home Index