---

Step * 1 5 1 1 1 1 1 2 1 1 1 1 1 1 2 1 1 1 2 1 1 of Lemma composition-term-uniformity

.....subterm..... T:t
3:n
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:H.𝕀(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(H.𝕀;A;I;i;rho;phi;u)
⟶ cubical-path-1(H.𝕀;A;I;i;rho;phi;u)
9. composition-uniformity(H.𝕀;A;cA)
10. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
11. I : fset(ℕ)
12. a : K(I)
13. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀
⊢ (tau+)(s(a);<new-name(I)>) = (s((tau)a);<new-name(I)>) ∈ H.𝕀(I+new-name(I))
BY
{ (CsmUnfoldingNotInterval THEN RepUR ``cube-context-adjoin`` 0 THEN EqCD) }

1
.....subterm..... T:t
1:n
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:H.𝕀(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(H.𝕀;A;I;i;rho;phi;u)
⟶ cubical-path-1(H.𝕀;A;I;i;rho;phi;u)
9. composition-uniformity(H.𝕀;A;cA)
10. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
11. I : fset(ℕ)
12. a : K(I)
13. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀
⊢ (tau I+new-name(I) s(a)) = s(tau I a) ∈ H(I+new-name(I))

2
.....subterm..... T:t
2:n
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:H.𝕀(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(H.𝕀;A;I;i;rho;phi;u)
⟶ cubical-path-1(H.𝕀;A;I;i;rho;phi;u)
9. composition-uniformity(H.𝕀;A;cA)
10. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
11. I : fset(ℕ)
12. a : K(I)
13. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀
⊢ <new-name(I)> = <new-name(I)> ∈ 𝕀(tau I+new-name(I) s(a))

3
.....eq aux..... 
1. H : CubicalSet{j}
2. K : CubicalSet{j}
3. tau : K j⟶ H
4. phi : {H ⊢ _:𝔽}
5. A : {H.𝕀 ⊢ _}
6. u : {H, phi.𝕀 ⊢ _:A}
7. a0 : {H ⊢ _:(A)[0(𝕀)][phi |⟶ (u)[0(𝕀)]]}
8. cA : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:H.𝕀(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(H.𝕀;A;I;i;rho;phi;u)
⟶ cubical-path-1(H.𝕀;A;I;i;rho;phi;u)
9. composition-uniformity(H.𝕀;A;cA)
10. ((phi)p)tau+ ∈ {K.𝕀 ⊢ _:𝔽}
11. I : fset(ℕ)
12. a : K(I)
13. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀
14. alpha : H(I+new-name(I))
⊢ istype(𝕀(alpha))

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  H  :  CubicalSet\{j\}
2.  K  :  CubicalSet\{j\}
3.  tau  :  K  j{}\mrightarrow{}  H
4.  phi  :  \{H  \mvdash{}  \_:\mBbbF{}\}
5.  A  :  \{H.\mBbbI{}  \mvdash{}  \_\}
6.  u  :  \{H,  phi.\mBbbI{}  \mvdash{}  \_:A\}
7.  a0  :  \{H  \mvdash{}  \_:(A)[0(\mBbbI{})][phi  |{}\mrightarrow{}  (u)[0(\mBbbI{})]]\}
8.  cA  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:H.\mBbbI{}(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
{}\mrightarrow{}  cubical-path-0(H.\mBbbI{};A;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(H.\mBbbI{};A;I;i;rho;phi;u)
9.  composition-uniformity(H.\mBbbI{};A;cA)
10.  ((phi)p)tau+  \mmember{}  \{K.\mBbbI{}  \mvdash{}  \_:\mBbbF{}\}
11.  I  :  fset(\mBbbN{})
12.  a  :  K(I)
13.  tau+  o  <(s(a);<new-name(I)>)>  \mmember{}  formal-cube(I+new-name(I))  j{}\mrightarrow{}  H.\mBbbI{}
\mvdash{}  (tau+)(s(a);<new-name(I)>)  =  (s((tau)a);<new-name(I)>)


By

---

Latex:
(CsmUnfoldingNotInterval  THEN  RepUR  ``cube-context-adjoin``  0  THEN  EqCD)

---

Home Index