---

Step * 1 4 1 of Lemma presheaf-elements_wf


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)} 
⊢ (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
= (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
∈ {f:cat-arrow(op-cat(C)) A4 A| (P A4 A f D1) = A1 ∈ (P A)} 
BY
{ ((InstLemma `cat-comp-assoc` [⌜op-cat(C)⌝;⌜A4⌝;⌜A3⌝;⌜A2⌝;⌜A⌝;⌜h⌝;⌜g⌝;⌜f⌝]⋅ THENA Auto)
   THEN (At ⌜Type⌝ EqTypeCD⋅ THENW 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)
⊢ (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f))
= (cat-comp(op-cat(C)) A4 A2 A (cat-comp(op-cat(C)) A4 A3 A2 h g) f)
∈ (cat-arrow(op-cat(C)) A4 A)

2
.....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)

---

Latex:

---

Latex:

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\} 
\mvdash{}  (cat-comp(op-cat(C))  A4  A3  A  h  (cat-comp(op-cat(C))  A3  A2  A  g  f))
=  (cat-comp(op-cat(C))  A4  A2  A  (cat-comp(op-cat(C))  A4  A3  A2  h  g)  f)


By

---

Latex:
((InstLemma  `cat-comp-assoc`  [\mkleeneopen{}op-cat(C)\mkleeneclose{};\mkleeneopen{}A4\mkleeneclose{};\mkleeneopen{}A3\mkleeneclose{};\mkleeneopen{}A2\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (At  \mkleeneopen{}Type\mkleeneclose{}  EqTypeCD\mcdot{}  THENW  Auto)
  )

---

Home Index