Step
*
1
of Lemma
comp-fun-to-comp-op_wf
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : composition-function{j:l,i:l}(Gamma;A)
4. I : fset(ℕ)
5. J : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ J}
8. g : J ⟶ I
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
13. ∀u:{formal-cube(I), canonical-section(();𝔽;I;⋅;phi).𝕀 ⊢ _:(A)<rho> o cube+(I;i)}.
∀a0:{formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[0(𝕀)][canonical-section(();𝔽;I;⋅;phi) |⟶ (u)[0(𝕀)]]}.
((comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) u a0)<g>
= (comp formal-cube(J) <rho> o cube+(I;i) o <g>+ (canonical-section(();𝔽;I;⋅;phi))<g> (u)<g>+ (a0)<g>)
∈ {formal-cube(J) ⊢ _:(((A)<rho> o cube+(I;i))[1(𝕀)])<g>[(canonical-section(();𝔽;I;⋅;phi))<g>
|⟶ ((u)[1(𝕀)])<g>]})
⊢ (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) (u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0)(1) (i1)(rho) g)
= comp formal-cube(J) <g,i=j(rho)> o cube+(J;j) canonical-section(();𝔽;J;⋅;g(phi))
((u)subset-trans(I+i;J+j;g,i=j;s(phi)))cube+(J;j)
canonical-section(Gamma;A;J;(j0)(g,i=j(rho));(a0 (i0)(rho) g))(1)
∈ A(g((i1)(rho)))
BY
{ ((Assert formal-cube(I+i), canonical-section(Gamma;𝔽;I+i;rho;s(phi)) = I+i,s(phi) ∈ CubicalSet{j} BY
(RWO "context-subset-is-cubical-subset" 0
THEN Auto
THEN EqCD
THEN Auto
THEN RepUR ``canonical-section cubical-term-at`` 0
THEN (RWO "face-type-ap-morph" 0 THENA Auto)
THEN (RWO "fl-morph-id" 0 THENA Auto)
THEN Reduce 0
THEN Auto))
THEN (Assert ⌜(u)cube+(I;i) ∈ {formal-cube(I), canonical-section(();𝔽;I;⋅;phi).𝕀 ⊢ _:(A)<rho> o cube+(I;i)}⌝⋅
THENA (BLemma `csm-ap-term-cube+` THEN Auto)
)
THEN (Assert canonical-section(Gamma;A;I;(i0)(rho);a0)
∈ {formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[0(𝕀)][canonical-section(();𝔽;I;⋅;phi)
|⟶ ((u)cube+(I;i))[0(𝕀)]]} BY
(BLemma `canonical-section-cubical-path-0` THEN Auto))
THEN (InstHyp [⌜(u)cube+(I;i)⌝;⌜canonical-section(Gamma;A;I;(i0)(rho);a0)⌝] (-4)⋅ THENA Auto)
THEN Thin (-5)) }
1
1. Gamma : CubicalSet{j}
2. A : {Gamma ⊢ _}
3. comp : composition-function{j:l,i:l}(Gamma;A)
4. I : fset(ℕ)
5. J : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I}
7. j : {j:ℕ| ¬j ∈ J}
8. g : J ⟶ I
9. rho : Gamma(I+i)
10. phi : 𝔽(I)
11. u : {I+i,s(phi) ⊢ _:(A)<rho> o iota}
12. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
13. formal-cube(I+i), canonical-section(Gamma;𝔽;I+i;rho;s(phi)) = I+i,s(phi) ∈ CubicalSet{j}
14. (u)cube+(I;i) ∈ {formal-cube(I), canonical-section(();𝔽;I;⋅;phi).𝕀 ⊢ _:(A)<rho> o cube+(I;i)}
15. canonical-section(Gamma;A;I;(i0)(rho);a0)
∈ {formal-cube(I) ⊢ _:((A)<rho> o cube+(I;i))[0(𝕀)][canonical-section(();𝔽;I;⋅;phi) |⟶ ((u)cube+(I;i))[0(𝕀)]]}
16. (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) (u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0))<g>
= (comp formal-cube(J) <rho> o cube+(I;i) o <g>+ (canonical-section(();𝔽;I;⋅;phi))<g> ((u)cube+(I;i))<g>+
(canonical-section(Gamma;A;I;(i0)(rho);a0))<g>)
∈ {formal-cube(J) ⊢ _:(((A)<rho> o cube+(I;i))[1(𝕀)])<g>[(canonical-section(();𝔽;I;⋅;phi))<g>
|⟶ (((u)cube+(I;i))[1(𝕀)])<g>]}
⊢ (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();𝔽;I;⋅;phi) (u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0)(1) (i1)(rho) g)
= comp formal-cube(J) <g,i=j(rho)> o cube+(J;j) canonical-section(();𝔽;J;⋅;g(phi))
((u)subset-trans(I+i;J+j;g,i=j;s(phi)))cube+(J;j)
canonical-section(Gamma;A;J;(j0)(g,i=j(rho));(a0 (i0)(rho) g))(1)
∈ A(g((i1)(rho)))
Latex:
Latex:
1. Gamma : CubicalSet\{j\}
2. A : \{Gamma \mvdash{} \_\}
3. comp : composition-function\{j:l,i:l\}(Gamma;A)
4. I : fset(\mBbbN{})
5. J : fset(\mBbbN{})
6. i : \{i:\mBbbN{}| \mneg{}i \mmember{} I\}
7. j : \{j:\mBbbN{}| \mneg{}j \mmember{} J\}
8. g : J {}\mrightarrow{} I
9. rho : Gamma(I+i)
10. phi : \mBbbF{}(I)
11. u : \{I+i,s(phi) \mvdash{} \_:(A)<rho> o iota\}
12. a0 : cubical-path-0(Gamma;A;I;i;rho;phi;u)
13. \mforall{}u:\{formal-cube(I), canonical-section(();\mBbbF{};I;\mcdot{};phi).\mBbbI{} \mvdash{} \_:(A)<rho> o cube+(I;i)\}.
\mforall{}a0:\{formal-cube(I) \mvdash{} \_:((A)<rho> o cube+(I;i))[0(\mBbbI{})][canonical-section(();\mBbbF{};I;\mcdot{};phi)
|{}\mrightarrow{} (u)[0(\mBbbI{})]]\}.
((comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();\mBbbF{};I;\mcdot{};phi) u a0)<g>
= (comp formal-cube(J) <rho> o cube+(I;i) o <g>+ (canonical-section(();\mBbbF{};I;\mcdot{};phi))<g> (u)<g>+
(a0)<g>))
\mvdash{} (comp formal-cube(I) <rho> o cube+(I;i) canonical-section(();\mBbbF{};I;\mcdot{};phi) (u)cube+(I;i)
canonical-section(Gamma;A;I;(i0)(rho);a0)(1) (i1)(rho) g)
= comp formal-cube(J) <g,i=j(rho)> o cube+(J;j) canonical-section(();\mBbbF{};J;\mcdot{};g(phi))
((u)subset-trans(I+i;J+j;g,i=j;s(phi)))cube+(J;j)
canonical-section(Gamma;A;J;(j0)(g,i=j(rho));(a0 (i0)(rho) g))(1)
By
Latex:
((Assert formal-cube(I+i), canonical-section(Gamma;\mBbbF{};I+i;rho;s(phi)) = I+i,s(phi) BY
(RWO "context-subset-is-cubical-subset" 0
THEN Auto
THEN EqCD
THEN Auto
THEN RepUR ``canonical-section cubical-term-at`` 0
THEN (RWO "face-type-ap-morph" 0 THENA Auto)
THEN (RWO "fl-morph-id" 0 THENA Auto)
THEN Reduce 0
THEN Auto))
THEN (Assert \mkleeneopen{}(u)cube+(I;i) \mmember{} \{formal-cube(I), canonical-section(();\mBbbF{};I;\mcdot{};phi).\mBbbI{} \mvdash{} \_
:(A)<rho> o cube+(I;i)\}\mkleeneclose{}\mcdot{}
THENA (BLemma `csm-ap-term-cube+` THEN Auto)
)
THEN (Assert canonical-section(Gamma;A;I;(i0)(rho);a0)
\mmember{} \{formal-cube(I) \mvdash{} \_:((A)<rho> o cube+(I;i))[0(\mBbbI{})][canonical-section(();\mBbbF{};I;\mcdot{};phi)
|{}\mrightarrow{} ((u)cube+(I;i))[0(\mBbbI{})]]\} BY
(BLemma `canonical-section-cubical-path-0` THEN Auto))
THEN (InstHyp [\mkleeneopen{}(u)cube+(I;i)\mkleeneclose{};\mkleeneopen{}canonical-section(Gamma;A;I;(i0)(rho);a0)\mkleeneclose{}] (-4)\mcdot{} THENA Auto)
THEN Thin (-5))
Home
Index