Step
*
2
1
2
1
of Lemma
poset-functor-extends-box-faces-1
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ (cube(bx[i1]) c flip(c;i2) (λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))))
BY
{ (InstLemma `nerve_box_edge_same1` [⌜cat(G)⌝;⌜I⌝;⌜J⌝;⌜x⌝;⌜i⌝;⌜bx⌝;⌜i2⌝;⌜((dimension(bx[i1]):=direction(bx[i1])) o c)⌝;
⌜bx[i1]⌝]⋅
THENA Try (QuickAuto)
)⋅ }
1
.....wf.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ i2 ∈ nameset(I)
2
.....wf.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ {c:name-morph(I;[])| (c i2) = 0 ∈ ℕ2}
3
.....antecedent.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ (∃j∈J. ¬(j = i2 ∈ Cname)) ∨ (((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℕ2) ∧ (¬↑null(J)))
4
.....wf.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ bx[i1] ∈ I-face(cubical-nerve(cat(G));I)
5
.....antecedent.....
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
⊢ (bx[i1] ∈ bx)
∧ (direction(bx[i1]) = (((dimension(bx[i1]):=direction(bx[i1])) o c) dimension(bx[i1])) ∈ ℕ2)
∧ (direction(bx[i1]) = (flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2) dimension(bx[i1])) ∈ ℕ2)
6
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-nerve(cat(G));I;J;x;i)
7. ¬↑null(J)
8. (∀j'∈J.j' = hd(J) ∈ Cname)
9. i1 : ℕ||bx||
10. ∀f:name-morph(I-[dimension(bx[i1])];[]). (((dimension(bx[i1]):=direction(bx[i1])) o f) ∈ name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : {c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0 ∈ ℕ2}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) ∈ name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0 ∈ ℕ2
15. ↑((((dimension(bx[i1]):=direction(bx[i1])) o c) x =z i) ∨b(¬beq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i ∈ ℤ) ∨ (¬(i2 = hd(J) ∈ Cname))
17. (cube(bx[i1]) ((dimension(bx[i1]):=direction(bx[i1])) o c) flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
(λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;flip(((dimension(bx[i1]):=direction(bx[i1])) o c);i2)))
⊢ (cube(bx[i1]) c flip(c;i2) (λx.Ax))
= nerve_box_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
∈ (cat-arrow(cat(G)) nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o c))
nerve_box_label(bx;((dimension(bx[i1]):=direction(bx[i1])) o flip(c;i2))))
Latex:
Latex:
1. G : Groupoid
2. I : Cname List
3. J : nameset(I) List
4. x : nameset(I)
5. i : \mBbbN{}2
6. bx : open\_box(cubical-nerve(cat(G));I;J;x;i)
7. \mneg{}\muparrow{}null(J)
8. (\mforall{}j'\mmember{}J.j' = hd(J))
9. i1 : \mBbbN{}||bx||
10. \mforall{}f:name-morph(I-[dimension(bx[i1])];[])
(((dimension(bx[i1]):=direction(bx[i1])) o f) \mmember{} name-morph(I;[]))
11. i2 : nameset(I-[dimension(bx[i1])])
12. c : \{c:name-morph(I-[dimension(bx[i1])];[])| (c i2) = 0\}
13. ((dimension(bx[i1]):=direction(bx[i1])) o c) \mmember{} name-morph(I;[])
14. (((dimension(bx[i1]):=direction(bx[i1])) o c) i2) = 0
15. \muparrow{}((((dimension(bx[i1]):=direction(bx[i1])) o c) x =\msubz{} i) \mvee{}\msubb{}(\mneg{}\msubb{}eq-cname(i2;hd(J))))
16. ((((dimension(bx[i1]):=direction(bx[i1])) o c) x) = i) \mvee{} (\mneg{}(i2 = hd(J)))
\mvdash{} (cube(bx[i1]) c flip(c;i2) (\mlambda{}x.Ax))
= nerve\_box\_edge(bx;((dimension(bx[i1]):=direction(bx[i1])) o c);i2)
By
Latex:
(InstLemma `nerve\_box\_edge\_same1` [\mkleeneopen{}cat(G)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}bx\mkleeneclose{};\mkleeneopen{}i2\mkleeneclose{};
\mkleeneopen{}((dimension(bx[i1]):=direction(bx[i1])) o c)\mkleeneclose{};\mkleeneopen{}bx[i1]\mkleeneclose{}]\mcdot{}
THENA Try (QuickAuto)
)\mcdot{}
Home
Index