---

Step * 1 4 1 2 of Lemma presheaf-elements_wf

.....set predicate..... 
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
7. A3 : cat-ob(op-cat(C))
8. z1 : P A3
9. A4 : cat-ob(op-cat(C))
10. D1 : P A4
11. f : {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
12. g : {f:cat-arrow(op-cat(C)) A3 A2| (P A3 A2 f z1) = B1 ∈ (P A2)} 
13. h : {f:cat-arrow(op-cat(C)) A4 A3| (P A4 A3 f D1) = z1 ∈ (P A3)} 
14. (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
= (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
∈ (cat-arrow(op-cat(C)) A4 A)
⊢ (P A4 A (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f)) D1) = A1 ∈ (P A)
BY
{ (InstLemma `functor-arrow-comp` [⌜parm{i'}⌝;⌜op-cat(C)⌝;⌜TypeCat⌝;⌜P⌝;⌜A4⌝;⌜A3⌝;⌜A⌝;⌜h⌝;
   ⌜cat-comp(op-cat(C)) A3 A2 A g f⌝]⋅
   THENA Auto
   ) }

1
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
7. A3 : cat-ob(op-cat(C))
8. z1 : P A3
9. A4 : cat-ob(op-cat(C))
10. D1 : P A4
11. f : {f:cat-arrow(op-cat(C)) A2 A| (P A2 A f B1) = A1 ∈ (P A)} 
12. g : {f:cat-arrow(op-cat(C)) A3 A2| (P A3 A2 f z1) = B1 ∈ (P A2)} 
13. h : {f:cat-arrow(op-cat(C)) A4 A3| (P A4 A3 f D1) = z1 ∈ (P A3)} 
14. (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
= (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
∈ (cat-arrow(op-cat(C)) A4 A)
15. (P A4 A (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f)))
= (cat-comp(TypeCat) (P A4) (P A3) (P A) (P A4 A3 h) (P A3 A (cat-comp(op-cat(C)) A3 A2 A g f)))
∈ (cat-arrow(TypeCat) (P A4) (P A))
⊢ (P A4 A (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f)) D1) = A1 ∈ (P A)

---

Latex:

---

Latex:
.....set  predicate..... 
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
7.  A3  :  cat-ob(op-cat(C))
8.  z1  :  P  A3
9.  A4  :  cat-ob(op-cat(C))
10.  D1  :  P  A4
11.  f  :  \{f:cat-arrow(op-cat(C))  A2  A|  (P  A2  A  f  B1)  =  A1\} 
12.  g  :  \{f:cat-arrow(op-cat(C))  A3  A2|  (P  A3  A2  f  z1)  =  B1\} 
13.  h  :  \{f:cat-arrow(op-cat(C))  A4  A3|  (P  A4  A3  f  D1)  =  z1\} 
14.  (cat-comp(op-cat(C))  A4  A2  A  (cat-comp(op-cat(C))  A4  A3  A2  h  g)  f)
=  (cat-comp(op-cat(C))  A4  A3  A  h  (cat-comp(op-cat(C))  A3  A2  A  g  f))
\mvdash{}  (P  A4  A  (cat-comp(op-cat(C))  A4  A3  A  h  (cat-comp(op-cat(C))  A3  A2  A  g  f))  D1)  =  A1


By

---

Latex:
(InstLemma  `functor-arrow-comp`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}op-cat(C)\mkleeneclose{};\mkleeneopen{}TypeCat\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}A4\mkleeneclose{};\mkleeneopen{}A3\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};
  \mkleeneopen{}cat-comp(op-cat(C))  A3  A2  A  g  f\mkleeneclose{}]\mcdot{}
  THENA  Auto
  )

---

Home Index