---

Step * 1 2 of Lemma presheaf-elements_wf

.....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)} 
BY
{ (((D 5 THEN D 4 THEN D 3 THEN All Reduce) THEN DSetVars) THEN At ⌜Type⌝ MemTypeCD⋅ THEN Auto) }

1
.....set predicate..... 
1. C : SmallCategory
2. P : Functor(op-cat(C);TypeCat)
3. A2 : cat-ob(op-cat(C))
4. A3 : P A2
5. A1 : cat-ob(op-cat(C))
6. B1 : P A1
7. A : cat-ob(op-cat(C))
8. D1 : P A
9. f : cat-arrow(op-cat(C)) A1 A2
10. (P A1 A2 f B1) = A3 ∈ (P A2)
11. g : cat-arrow(op-cat(C)) A A1
12. (P A A1 g D1) = B1 ∈ (P A1)
⊢ (P A A2 (cat-comp(op-cat(C)) A A1 A2 g f) D1) = A3 ∈ (P A2)

---

Latex:

---

Latex:
.....subterm.....  T:t
4:n
1.  C  :  SmallCategory
2.  P  :  Functor(op-cat(C);TypeCat)
3.  Aa  :  A:cat-ob(op-cat(C))  \mtimes{}  (P  A)
4.  Bb  :  A:cat-ob(op-cat(C))  \mtimes{}  (P  A)
5.  Dd  :  A:cat-ob(op-cat(C))  \mtimes{}  (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\} 
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\} 
\mvdash{}  cat-comp(op-cat(C))  (fst(Dd))  (fst(Bb))  (fst(Aa))  g  f  \mmember{}  let  A,a  =  Aa 
                                                                                                                    in  let  B,b  =  Dd 
                                                                                                                          in  \{f:cat-arrow(op-cat(C))  B  A| 
                                                                                                                                  (P  B  A  f  b)  =  a\} 


By

---

Latex:
(((D  5  THEN  D  4  THEN  D  3  THEN  All  Reduce)  THEN  DSetVars)  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}  THEN  Auto)

---

Home Index