Step
*
1
of Lemma
poset-extend-unique
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. let F,M = <F1, F2>
in (∀x:cat-ob(poset-cat(I)). ((M 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.
((M x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (M x y f) (M y z g))
∈ (cat-arrow(C) (F x) (F 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. let F,M = <F, G1>
in (∀x:cat-ob(poset-cat(I)). ((M 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.
((M x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (M x y f) (M 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))))
15. x : cat-ob(poset-cat(I))
16. y : cat-ob(poset-cat(I))
17. x1 : cat-arrow(poset-cat(I)) x y
⊢ (F2 x y x1) = (G1 x y x1) ∈ (cat-arrow(C) (F1 x) (F1 y))
BY
{ TACTIC:(All Reduce
THEN (Assert ⌜∀d:ℕ. ∀x,y:cat-ob(poset-cat(I)). ∀p:cat-arrow(poset-cat(I)) x y.
((poset-cat-dist(I;x;y) ≤ d) ⇒ ((F2 x y p) = (G1 x y p) ∈ (cat-arrow(C) (F1 x) (F1 y))))⌝⋅
THENM (InstHyp [⌜poset-cat-dist(I;x;y)⌝;⌜x⌝;⌜y⌝;⌜x1⌝] (-1)⋅ THEN Auto)
)
THEN RepeatFor 3 (Thin (-1))
THEN Assert ⌜∀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))))⌝
⋅) }
1
.....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))))
2
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))))
15. ∀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))))
⊢ ∀d:ℕ. ∀x,y:cat-ob(poset-cat(I)). ∀p:cat-arrow(poset-cat(I)) x y.
((poset-cat-dist(I;x;y) ≤ d) ⇒ ((F2 x y p) = (G1 x y p) ∈ (cat-arrow(C) (F1 x) (F1 y))))
Latex:
Latex:
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. let F,M = <F1, F2>
in (\mforall{}x:cat-ob(poset-cat(I)). ((M 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.
((M x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (M x y f) (M 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. let F,M = <F, G1>
in (\mforall{}x:cat-ob(poset-cat(I)). ((M 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.
((M x z (cat-comp(poset-cat(I)) x y z f g))
= (cat-comp(C) (F x) (F y) (F z) (M x y f) (M 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))
15. x : cat-ob(poset-cat(I))
16. y : cat-ob(poset-cat(I))
17. x1 : cat-arrow(poset-cat(I)) x y
\mvdash{} (F2 x y x1) = (G1 x y x1)
By
Latex:
TACTIC:(All Reduce
THEN (Assert \mkleeneopen{}\mforall{}d:\mBbbN{}. \mforall{}x,y:cat-ob(poset-cat(I)). \mforall{}p:cat-arrow(poset-cat(I)) x y.
((poset-cat-dist(I;x;y) \mleq{} d) {}\mRightarrow{} ((F2 x y p) = (G1 x y p)))\mkleeneclose{}\mcdot{}
THENM (InstHyp [\mkleeneopen{}poset-cat-dist(I;x;y)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}] (-1)\mcdot{} THEN Auto)
)
THEN RepeatFor 3 (Thin (-1))
THEN Assert \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{})
Home
Index