Step
*
1
1
2
of Lemma
cubical-interval-filler-fills
1. I : Cname List
2. J : nameset(I) List
3. ¬(J = [] ∈ (nameset(I) List))
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-interval();I;J;x;i)
7. j : ℕ||bx||
8. nameset(J) ⊆r nameset(I)
9. y : nameset(J)
10. hd(J) = y ∈ nameset(J)
⊢ is-face(cubical-interval();I;λL.cube(get_face(y;L y;bx))(L);bx[j])
BY
{ (RepUR ``is-face cube-set-restriction cubical-interval I-cube functor-ob`` 0 THEN (FunExt THENA Auto) THEN Reduce 0) }
1
1. I : Cname List
2. J : nameset(I) List
3. ¬(J = [] ∈ (nameset(I) List))
4. x : nameset(I)
5. i : ℕ2
6. bx : open_box(cubical-interval();I;J;x;i)
7. j : ℕ||bx||
8. nameset(J) ⊆r nameset(I)
9. y : nameset(J)
10. hd(J) = y ∈ nameset(J)
11. x1 : name-morph(I-[dimension(bx[j])];[])
⊢ cube(get_face(y;((dimension(bx[j]):=direction(bx[j])) o x1) y;bx))(((dimension(bx[j]):=direction(bx[j])) o x1))
= (cube(bx[j]) x1)
∈ ℕ2
Latex:
Latex:
1. I : Cname List
2. J : nameset(I) List
3. \mneg{}(J = [])
4. x : nameset(I)
5. i : \mBbbN{}2
6. bx : open\_box(cubical-interval();I;J;x;i)
7. j : \mBbbN{}||bx||
8. nameset(J) \msubseteq{}r nameset(I)
9. y : nameset(J)
10. hd(J) = y
\mvdash{} is-face(cubical-interval();I;\mlambda{}L.cube(get\_face(y;L y;bx))(L);bx[j])
By
Latex:
(RepUR ``is-face cube-set-restriction cubical-interval I-cube functor-ob`` 0
THEN (FunExt THENA Auto)
THEN Reduce 0)
Home
Index