Step
*
1
4
1
2
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)}
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)
BY
{ (RepUR ``type-cat`` -1 THEN ApFunToHypEquands `Z' ⌜Z D1⌝ ⌜P A⌝ (-1)⋅ THEN 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)))
= ((P A3 A (cat-comp(op-cat(C)) A3 A2 A g f)) o (P A4 A3 h))
∈ ((P A4) ⟶ (P A))
16. (P A4 A (cat-comp(op-cat(C)) A4 A3 A h (cat-comp(op-cat(C)) A3 A2 A g f)) D1)
= (((P A3 A (cat-comp(op-cat(C)) A3 A2 A g f)) o (P A4 A3 h)) D1)
∈ (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:
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))
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)))
\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:
(RepUR ``type-cat`` -1 THEN ApFunToHypEquands `Z' \mkleeneopen{}Z D1\mkleeneclose{} \mkleeneopen{}P A\mkleeneclose{} (-1)\mcdot{} THEN Auto)
Home
Index