---

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

.....assertion..... 
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. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)), ((phi)p)tau+ o <(s(a);<new-name(I)>)> j⟶ H.𝕀, (phi)p
15. {formal-cube(I+new-name(I)), ((phi)p)tau+ o <(s(a);<new-name(I)>)> ⊢ _:(A)tau+ o <(s(a);<new-name(I)>)>}
= {I+new-name(I),s(phi((tau)a)) ⊢ _:(A)<(s((tau)a);<new-name(I)>)> o iota}
∈ 𝕌{[i | j']}
⊢ tau+ o <(s(a);<new-name(I)>)> = <(s((tau)a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀
BY
{ (RWO "csm-comp-context-map" 0
   THENA (Auto THEN (RWO "interval-type-at" 0 THENA Auto) THEN RepUR ``interval-presheaf`` 0 THEN Auto)
   ) }

1
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. tau+ o <(s(a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)), ((phi)p)tau+ o <(s(a);<new-name(I)>)> j⟶ H.𝕀, (phi)p
15. {formal-cube(I+new-name(I)), ((phi)p)tau+ o <(s(a);<new-name(I)>)> ⊢ _:(A)tau+ o <(s(a);<new-name(I)>)>}
= {I+new-name(I),s(phi((tau)a)) ⊢ _:(A)<(s((tau)a);<new-name(I)>)> o iota}
∈ 𝕌{[i | j']}
⊢ <(tau+)(s(a);<new-name(I)>)> = <(s((tau)a);<new-name(I)>)> ∈ formal-cube(I+new-name(I)) j⟶ H.𝕀

---

Latex:

---

Latex:
.....assertion..... 
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{}
14.  tau+  o  <(s(a);<new-name(I)>)>
        \mmember{}  formal-cube(I+new-name(I)),  ((phi)p)tau+  o  <(s(a);<new-name(I)>)>  j{}\mrightarrow{}  H.\mBbbI{},  (phi)p
15.  \{formal-cube(I+new-name(I)),  ((phi)p)tau+  o  <(s(a);<new-name(I)>)>  \mvdash{}  \_
          :(A)tau+  o  <(s(a);<new-name(I)>)>\}
=  \{I+new-name(I),s(phi((tau)a))  \mvdash{}  \_:(A)<(s((tau)a);<new-name(I)>)>  o  iota\}
\mvdash{}  tau+  o  <(s(a);<new-name(I)>)>  =  <(s((tau)a);<new-name(I)>)>


By

---

Latex:
(RWO  "csm-comp-context-map"  0
  THENA  (Auto
                THEN  (RWO  "interval-type-at"  0  THENA  Auto)
                THEN  RepUR  ``interval-presheaf``  0
                THEN  Auto)
  )

---

Home Index