Step
*
1
1
1
of Lemma
same-face-edge-arrows-commute
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : ℕ2
8. F : cat-ob(poset-cat(I-[j])) ⟶ cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
⟶ y:cat-ob(poset-cat(I-[j]))
⟶ (cat-arrow(poset-cat(I-[j])) x@0 y)
⟶ (cat-arrow(C) (F x@0) (F y))
10. (∀x@0:cat-ob(poset-cat(I-[j]))
((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0)) ∈ (cat-arrow(C) (F x@0) (F x@0))))
∧ (∀x@0,y,z:cat-ob(poset-cat(I-[j])). ∀f:cat-arrow(poset-cat(I-[j])) x@0 y. ∀g:cat-arrow(poset-cat(I-[j])) y z.
((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
= (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))
∈ (cat-arrow(C) (F x@0) (F z))))
11. (f a) = 0 ∈ ℕ2
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(j = a ∈ Cname)
15. ¬(j = b ∈ Cname)
16. ∀x,y,z:name-morph(I-[j];[]).
((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
⇒ ((H x z (λx.Ax))
= (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
∈ (cat-arrow(C) (F x) (F z))))
17. f ∈ name-morph(I-[j];[])
18. flip(f;a) ∈ name-morph(I-[j];[])
19. flip(f;b) ∈ name-morph(I-[j];[])
20. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
21. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
⊢ (cat-comp(C) (F f) (F flip(f;a)) (F flip(flip(f;a);b)) (H f flip(f;a) (λx.Ax))
(H flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (F f) (F flip(f;b)) (F flip(flip(f;b);a)) (H f flip(f;b) (λx.Ax))
(H flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (F f) (F flip(flip(f;a);b)))
BY
{ (InstHyp [⌜f⌝;⌜flip(f;a)⌝; ⌜flip(flip(f;a);b)⌝] (-6)⋅ THENA Auto) }
1
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : ℕ2
8. F : cat-ob(poset-cat(I-[j])) ⟶ cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
⟶ y:cat-ob(poset-cat(I-[j]))
⟶ (cat-arrow(poset-cat(I-[j])) x@0 y)
⟶ (cat-arrow(C) (F x@0) (F y))
10. ∀x@0:cat-ob(poset-cat(I-[j]))
((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0)) ∈ (cat-arrow(C) (F x@0) (F x@0)))
11. ∀x@0,y,z:cat-ob(poset-cat(I-[j])). ∀f:cat-arrow(poset-cat(I-[j])) x@0 y. ∀g:cat-arrow(poset-cat(I-[j])) y z.
((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
= (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))
∈ (cat-arrow(C) (F x@0) (F z)))
12. (f a) = 0 ∈ ℕ2
13. (f b) = 0 ∈ ℕ2
14. ¬(a = b ∈ nameset(I))
15. ¬(j = a ∈ Cname)
16. ¬(j = b ∈ Cname)
17. ∀x,y,z:name-morph(I-[j];[]).
((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
⇒ ((H x z (λx.Ax))
= (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
∈ (cat-arrow(C) (F x) (F z))))
18. f ∈ name-morph(I-[j];[])
19. flip(f;a) ∈ name-morph(I-[j];[])
20. flip(f;b) ∈ name-morph(I-[j];[])
21. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
22. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
23. i : nameset(I-[j])
⊢ (f i) ≤ (flip(f;a) i)
2
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : ℕ2
8. F : cat-ob(poset-cat(I-[j])) ⟶ cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
⟶ y:cat-ob(poset-cat(I-[j]))
⟶ (cat-arrow(poset-cat(I-[j])) x@0 y)
⟶ (cat-arrow(C) (F x@0) (F y))
10. ∀x@0:cat-ob(poset-cat(I-[j]))
((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0)) ∈ (cat-arrow(C) (F x@0) (F x@0)))
11. ∀x@0,y,z:cat-ob(poset-cat(I-[j])). ∀f:cat-arrow(poset-cat(I-[j])) x@0 y. ∀g:cat-arrow(poset-cat(I-[j])) y z.
((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
= (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))
∈ (cat-arrow(C) (F x@0) (F z)))
12. (f a) = 0 ∈ ℕ2
13. (f b) = 0 ∈ ℕ2
14. ¬(a = b ∈ nameset(I))
15. ¬(j = a ∈ Cname)
16. ¬(j = b ∈ Cname)
17. ∀x,y,z:name-morph(I-[j];[]).
((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
⇒ ((H x z (λx.Ax))
= (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
∈ (cat-arrow(C) (F x) (F z))))
18. f ∈ name-morph(I-[j];[])
19. flip(f;a) ∈ name-morph(I-[j];[])
20. flip(f;b) ∈ name-morph(I-[j];[])
21. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
22. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
23. i : nameset(I-[j])
⊢ (flip(f;a) i) ≤ (flip(flip(f;a);b) i)
3
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : ℕ2
8. F : cat-ob(poset-cat(I-[j])) ⟶ cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
⟶ y:cat-ob(poset-cat(I-[j]))
⟶ (cat-arrow(poset-cat(I-[j])) x@0 y)
⟶ (cat-arrow(C) (F x@0) (F y))
10. (∀x@0:cat-ob(poset-cat(I-[j]))
((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0)) ∈ (cat-arrow(C) (F x@0) (F x@0))))
∧ (∀x@0,y,z:cat-ob(poset-cat(I-[j])). ∀f:cat-arrow(poset-cat(I-[j])) x@0 y. ∀g:cat-arrow(poset-cat(I-[j])) y z.
((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
= (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))
∈ (cat-arrow(C) (F x@0) (F z))))
11. (f a) = 0 ∈ ℕ2
12. (f b) = 0 ∈ ℕ2
13. ¬(a = b ∈ nameset(I))
14. ¬(j = a ∈ Cname)
15. ¬(j = b ∈ Cname)
16. ∀x,y,z:name-morph(I-[j];[]).
((∀i:nameset(I-[j]). ((x i) ≤ (y i)))
⇒ (∀i:nameset(I-[j]). ((y i) ≤ (z i)))
⇒ ((H x z (λx.Ax))
= (cat-comp(C) (F x) (F y) (F z) (H x y (λi.Ax)) (H y z (λi.Ax)))
∈ (cat-arrow(C) (F x) (F z))))
17. f ∈ name-morph(I-[j];[])
18. flip(f;a) ∈ name-morph(I-[j];[])
19. flip(f;b) ∈ name-morph(I-[j];[])
20. flip(flip(f;a);b) ∈ name-morph(I-[j];[])
21. flip(flip(f;b);a) ∈ name-morph(I-[j];[])
22. (H f flip(flip(f;a);b) (λx.Ax))
= (cat-comp(C) (F f) (F flip(f;a)) (F flip(flip(f;a);b)) (H f flip(f;a) (λi.Ax))
(H flip(f;a) flip(flip(f;a);b) (λi.Ax)))
∈ (cat-arrow(C) (F f) (F flip(flip(f;a);b)))
⊢ (cat-comp(C) (F f) (F flip(f;a)) (F flip(flip(f;a);b)) (H f flip(f;a) (λx.Ax))
(H flip(f;a) flip(flip(f;a);b) (λx.Ax)))
= (cat-comp(C) (F f) (F flip(f;b)) (F flip(flip(f;b);a)) (H f flip(f;b) (λx.Ax))
(H flip(f;b) flip(flip(f;b);a) (λx.Ax)))
∈ (cat-arrow(C) (F f) (F flip(flip(f;a);b)))
Latex:
Latex:
1. C : SmallCategory
2. I : Cname List
3. f : name-morph(I;[])
4. a : nameset(I)
5. b : nameset(I)
6. j : nameset(I)
7. v2 : \mBbbN{}2
8. F : cat-ob(poset-cat(I-[j])) {}\mrightarrow{} cat-ob(C)
9. H : x@0:cat-ob(poset-cat(I-[j]))
{}\mrightarrow{} y:cat-ob(poset-cat(I-[j]))
{}\mrightarrow{} (cat-arrow(poset-cat(I-[j])) x@0 y)
{}\mrightarrow{} (cat-arrow(C) (F x@0) (F y))
10. (\mforall{}x@0:cat-ob(poset-cat(I-[j]))
((H x@0 x@0 (cat-id(poset-cat(I-[j])) x@0)) = (cat-id(C) (F x@0))))
\mwedge{} (\mforall{}x@0,y,z:cat-ob(poset-cat(I-[j])). \mforall{}f:cat-arrow(poset-cat(I-[j])) x@0 y.
\mforall{}g:cat-arrow(poset-cat(I-[j])) y z.
((H x@0 z (cat-comp(poset-cat(I-[j])) x@0 y z f g))
= (cat-comp(C) (F x@0) (F y) (F z) (H x@0 y f) (H y z g))))
11. (f a) = 0
12. (f b) = 0
13. \mneg{}(a = b)
14. \mneg{}(j = a)
15. \mneg{}(j = b)
16. \mforall{}x,y,z:name-morph(I-[j];[]).
((\mforall{}i:nameset(I-[j]). ((x i) \mleq{} (y i)))
{}\mRightarrow{} (\mforall{}i:nameset(I-[j]). ((y i) \mleq{} (z i)))
{}\mRightarrow{} ((H x z (\mlambda{}x.Ax)) = (cat-comp(C) (F x) (F y) (F z) (H x y (\mlambda{}i.Ax)) (H y z (\mlambda{}i.Ax)))))
17. f \mmember{} name-morph(I-[j];[])
18. flip(f;a) \mmember{} name-morph(I-[j];[])
19. flip(f;b) \mmember{} name-morph(I-[j];[])
20. flip(flip(f;a);b) \mmember{} name-morph(I-[j];[])
21. flip(flip(f;b);a) \mmember{} name-morph(I-[j];[])
\mvdash{} (cat-comp(C) (F f) (F flip(f;a)) (F flip(flip(f;a);b)) (H f flip(f;a) (\mlambda{}x.Ax))
(H flip(f;a) flip(flip(f;a);b) (\mlambda{}x.Ax)))
= (cat-comp(C) (F f) (F flip(f;b)) (F flip(flip(f;b);a)) (H f flip(f;b) (\mlambda{}x.Ax))
(H flip(f;b) flip(flip(f;b);a) (\mlambda{}x.Ax)))
By
Latex:
(InstHyp [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}flip(f;a)\mkleeneclose{}; \mkleeneopen{}flip(flip(f;a);b)\mkleeneclose{}] (-6)\mcdot{} THENA Auto)
Home
Index