---

Step * 1 2 1 of Lemma presheaf-elements_wf

.....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)
BY
{ (InstLemma `functor-arrow-comp` [⌜parm{i'}⌝;⌜op-cat(C)⌝;⌜TypeCat⌝;⌜P⌝;⌜A⌝;⌜A1⌝;⌜A2⌝;⌜g⌝;⌜f⌝]⋅ THENA Auto) }

1
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)
13. (P A A2 (cat-comp(op-cat(C)) A A1 A2 g f))
= (cat-comp(TypeCat) (P A) (P A1) (P A2) (P A A1 g) (P A1 A2 f))
∈ (cat-arrow(TypeCat) (P A) (P A2))
⊢ (P A A2 (cat-comp(op-cat(C)) A A1 A2 g f) D1) = A3 ∈ (P A2)

---

Latex:

---

Latex:
.....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
11.  g  :  cat-arrow(op-cat(C))  A  A1
12.  (P  A  A1  g  D1)  =  B1
\mvdash{}  (P  A  A2  (cat-comp(op-cat(C))  A  A1  A2  g  f)  D1)  =  A3


By

---

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

---

Home Index