Step
*
2
1
of Lemma
poset-functor-extends_wf
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:name-morph(I;[]) ⟶ y:name-morph(I;[]) ⟶ (∀x@0:nameset(I). (↑x x@0 ≤z y x@0)) ⟶ (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. ob(<F1, F2>) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
9. i : nameset(I)
10. c : {c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}
⊢ F2 c flip(c;i) (λx.Ax) ∈ cat-arrow(C) (L c) (L flip(c;i))
BY
{ DoSubsume }
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:name-morph(I;[]) ⟶ y:name-morph(I;[]) ⟶ (∀x@0:nameset(I). (↑x x@0 ≤z y x@0)) ⟶ (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. ob(<F1, F2>) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
9. i : nameset(I)
10. c : {c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}
⊢ F2 c flip(c;i) (λx.Ax) ∈ cat-arrow(C) (F1 c) (F1 flip(c;i))
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:name-morph(I;[]) ⟶ y:name-morph(I;[]) ⟶ (∀x@0:nameset(I). (↑x x@0 ≤z y x@0)) ⟶ (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. ob(<F1, F2>) = L ∈ (name-morph(I;[]) ⟶ cat-ob(C))
9. i : nameset(I)
10. c : {c:name-morph(I;[])| (c i) = 0 ∈ ℕ2}
11. (F2 c flip(c;i) (λx.Ax)) = (F2 c flip(c;i) (λx.Ax)) ∈ (cat-arrow(C) (F1 c) (F1 flip(c;i)))
⊢ (cat-arrow(C) (F1 c) (F1 flip(c;i))) ⊆r (cat-arrow(C) (L c) (L flip(c;i)))
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:name-morph(I;[])
{}\mrightarrow{} y:name-morph(I;[])
{}\mrightarrow{} (\mforall{}x@0:nameset(I). (\muparrow{}x x@0 \mleq{}z y x@0))
{}\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. ob(<F1, F2>) = L
9. i : nameset(I)
10. c : \{c:name-morph(I;[])| (c i) = 0\}
\mvdash{} F2 c flip(c;i) (\mlambda{}x.Ax) \mmember{} cat-arrow(C) (L c) (L flip(c;i))
By
Latex:
DoSubsume
Home
Index