Step
*
1
1
of Lemma
poset-extend-unique
.....assertion.....
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. F1 : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
6. F2 : x:cat-ob(poset-cat(I))
⟶ y:cat-ob(poset-cat(I))
⟶ (cat-arrow(poset-cat(I)) x y)
⟶ (cat-arrow(C) (F1 x) (F1 y))
7. (∀x:cat-ob(poset-cat(I)). ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x))))
∧ (∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
((F2 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F1 x) (F1 y) (F1 z) (F2 x y f) (F2 y z g))
∈ (cat-arrow(C) (F1 x) (F1 z))))
8. F : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
9. G1 : x:cat-ob(poset-cat(I)) ⟶ y:cat-ob(poset-cat(I)) ⟶ (cat-arrow(poset-cat(I)) x y) ⟶ (cat-arrow(C) (F x) (F y))
10. (∀x:cat-ob(poset-cat(I)). ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x))))
∧ (∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
((G1 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (G1 x y f) (G1 y z g))
∈ (cat-arrow(C) (F x) (F z))))
11. F1 = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
12. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
((F2 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
13. F = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
14. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
((G1 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
⊢ ∀x,y:cat-ob(poset-cat(I)). ∀p:cat-arrow(poset-cat(I)) x y.
((x = y ∈ cat-ob(poset-cat(I))) ⇒ ((F2 x y p) = (G1 x y p) ∈ (cat-arrow(C) (F1 x) (F1 y))))
BY
{ TACTIC:(Auto
THEN (Assert ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x)))
∧ ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x))) BY
Auto)
THEN (Assert ⌜(F2 x x (cat-id(poset-cat(I)) x))
= (G1 x x (cat-id(poset-cat(I)) x))
∈ (cat-arrow(C) (F1 x) (F1 x))⌝⋅
THENA Auto
)) }
1
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) ⟶ cat-ob(C)
4. E : i:nameset(I) ⟶ c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} ⟶ (cat-arrow(C) (L c) (L flip(c;i)))
5. F1 : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
6. F2 : x:cat-ob(poset-cat(I))
⟶ y:cat-ob(poset-cat(I))
⟶ (cat-arrow(poset-cat(I)) x y)
⟶ (cat-arrow(C) (F1 x) (F1 y))
7. ∀x:cat-ob(poset-cat(I)). ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x)))
8. ∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
((F2 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F1 x) (F1 y) (F1 z) (F2 x y f) (F2 y z g))
∈ (cat-arrow(C) (F1 x) (F1 z)))
9. F : cat-ob(poset-cat(I)) ⟶ cat-ob(C)
10. G1 : x:cat-ob(poset-cat(I)) ⟶ y:cat-ob(poset-cat(I)) ⟶ (cat-arrow(poset-cat(I)) x y) ⟶ (cat-arrow(C) (F x) (F y))
11. ∀x:cat-ob(poset-cat(I)). ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x)))
12. ∀x,y,z:cat-ob(poset-cat(I)). ∀f:cat-arrow(poset-cat(I)) x y. ∀g:cat-arrow(poset-cat(I)) y z.
((G1 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (G1 x y f) (G1 y z g))
∈ (cat-arrow(C) (F x) (F z)))
13. F1 = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
14. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
((F2 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
15. F = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
16. ∀i:nameset(I). ∀c:{c:name-morph(I;[])| (c i) = 0 ∈ ℕ2} .
((G1 c flip(c;i) (λx.Ax)) = (E i c) ∈ (cat-arrow(C) (L c) (L flip(c;i))))
17. x : cat-ob(poset-cat(I))@i
18. y : cat-ob(poset-cat(I))@i
19. p : cat-arrow(poset-cat(I)) x y@i
20. x = y ∈ cat-ob(poset-cat(I))
21. ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)) ∈ (cat-arrow(C) (F1 x) (F1 x)))
∧ ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x)) ∈ (cat-arrow(C) (F x) (F x)))
22. (F2 x x (cat-id(poset-cat(I)) x)) = (G1 x x (cat-id(poset-cat(I)) x)) ∈ (cat-arrow(C) (F1 x) (F1 x))
⊢ (F2 x y p) = (G1 x y p) ∈ (cat-arrow(C) (F1 x) (F1 y))
Latex:
Latex:
.....assertion.....
1. C : SmallCategory
2. I : Cname List
3. L : name-morph(I;[]) {}\mrightarrow{} cat-ob(C)
4. E : i:nameset(I) {}\mrightarrow{} c:\{c:name-morph(I;[])| (c i) = 0\} {}\mrightarrow{} (cat-arrow(C) (L c) (L flip(c;i)))
5. F1 : cat-ob(poset-cat(I)) {}\mrightarrow{} cat-ob(C)
6. F2 : x:cat-ob(poset-cat(I))
{}\mrightarrow{} y:cat-ob(poset-cat(I))
{}\mrightarrow{} (cat-arrow(poset-cat(I)) x y)
{}\mrightarrow{} (cat-arrow(C) (F1 x) (F1 y))
7. (\mforall{}x:cat-ob(poset-cat(I)). ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x))))
\mwedge{} (\mforall{}x,y,z:cat-ob(poset-cat(I)). \mforall{}f:cat-arrow(poset-cat(I)) x y. \mforall{}g:cat-arrow(poset-cat(I)) y z.
((F2 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F1 x) (F1 y) (F1 z) (F2 x y f) (F2 y z g))))
8. F : cat-ob(poset-cat(I)) {}\mrightarrow{} cat-ob(C)
9. G1 : x:cat-ob(poset-cat(I))
{}\mrightarrow{} y:cat-ob(poset-cat(I))
{}\mrightarrow{} (cat-arrow(poset-cat(I)) x y)
{}\mrightarrow{} (cat-arrow(C) (F x) (F y))
10. (\mforall{}x:cat-ob(poset-cat(I)). ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x))))
\mwedge{} (\mforall{}x,y,z:cat-ob(poset-cat(I)). \mforall{}f:cat-arrow(poset-cat(I)) x y. \mforall{}g:cat-arrow(poset-cat(I)) y z.
((G1 x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (G1 x y f) (G1 y z g))))
11. F1 = L
12. \mforall{}i:nameset(I). \mforall{}c:\{c:name-morph(I;[])| (c i) = 0\} . ((F2 c flip(c;i) (\mlambda{}x.Ax)) = (E i c))
13. F = L
14. \mforall{}i:nameset(I). \mforall{}c:\{c:name-morph(I;[])| (c i) = 0\} . ((G1 c flip(c;i) (\mlambda{}x.Ax)) = (E i c))
\mvdash{} \mforall{}x,y:cat-ob(poset-cat(I)). \mforall{}p:cat-arrow(poset-cat(I)) x y. ((x = y) {}\mRightarrow{} ((F2 x y p) = (G1 x y p)))
By
Latex:
TACTIC:(Auto
THEN (Assert ((F2 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F1 x)))
\mwedge{} ((G1 x x (cat-id(poset-cat(I)) x)) = (cat-id(C) (F x))) BY
Auto)
THEN (Assert \mkleeneopen{}(F2 x x (cat-id(poset-cat(I)) x)) = (G1 x x (cat-id(poset-cat(I)) x))\mkleeneclose{}\mcdot{}
THENA Auto
))
Home
Index