---

Step * 1 of Lemma csm-composition-comp


1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. Z : CubicalSet{j}
4. s1 : Z j⟶ Y
5. s2 : Y j⟶ X
6. A : {X ⊢ _}
7. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:X(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(X;A;I;i;rho;phi;u)
⟶ cubical-path-1(X;A;I;i;rho;phi;u)
8. composition-uniformity(X;A;comp)
9. I : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. rho : Z(I+i)
12. phi : 𝔽(I)
13. u : {I+i,s(phi) ⊢ _:((A)s2 o s1)<rho> o iota}
14. x : cubical-path-0(Z;(A)s2 o s1;I;i;rho;phi;u)
⊢ (comp I i (s2)(s1)rho phi u x) = (comp I i (s2 o s1)rho phi u x) ∈ cubical-path-1(Z;(A)s2 o s1;I;i;rho;phi;u)
BY
{ SubsumeC ⌜cubical-path-1(X;A;I;i;(s2 o s1)rho;phi;u)⌝⋅ }

1
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. Z : CubicalSet{j}
4. s1 : Z j⟶ Y
5. s2 : Y j⟶ X
6. A : {X ⊢ _}
7. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:X(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(X;A;I;i;rho;phi;u)
⟶ cubical-path-1(X;A;I;i;rho;phi;u)
8. composition-uniformity(X;A;comp)
9. I : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. rho : Z(I+i)
12. phi : 𝔽(I)
13. u : {I+i,s(phi) ⊢ _:((A)s2 o s1)<rho> o iota}
14. x : cubical-path-0(Z;(A)s2 o s1;I;i;rho;phi;u)
⊢ (comp I i (s2)(s1)rho phi u x) = (comp I i (s2 o s1)rho phi u x) ∈ cubical-path-1(X;A;I;i;(s2 o s1)rho;phi;u)

2
1. X : CubicalSet{j}
2. Y : CubicalSet{j}
3. Z : CubicalSet{j}
4. s1 : Z j⟶ Y
5. s2 : Y j⟶ X
6. A : {X ⊢ _}
7. comp : I:fset(ℕ)
⟶ i:{i:ℕ| ¬i ∈ I} 
⟶ rho:X(I+i)
⟶ phi:𝔽(I)
⟶ u:{I+i,s(phi) ⊢ _:(A)<rho> o iota}
⟶ cubical-path-0(X;A;I;i;rho;phi;u)
⟶ cubical-path-1(X;A;I;i;rho;phi;u)
8. composition-uniformity(X;A;comp)
9. I : fset(ℕ)
10. i : {i:ℕ| ¬i ∈ I} 
11. rho : Z(I+i)
12. phi : 𝔽(I)
13. u : {I+i,s(phi) ⊢ _:((A)s2 o s1)<rho> o iota}
14. x : cubical-path-0(Z;(A)s2 o s1;I;i;rho;phi;u)
15. (comp I i (s2)(s1)rho phi u x) = (comp I i (s2 o s1)rho phi u x) ∈ cubical-path-1(X;A;I;i;(s2 o s1)rho;phi;u)
⊢ cubical-path-1(X;A;I;i;(s2 o s1)rho;phi;u) ⊆r cubical-path-1(Z;(A)s2 o s1;I;i;rho;phi;u)

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  Y  :  CubicalSet\{j\}
3.  Z  :  CubicalSet\{j\}
4.  s1  :  Z  j{}\mrightarrow{}  Y
5.  s2  :  Y  j{}\mrightarrow{}  X
6.  A  :  \{X  \mvdash{}  \_\}
7.  comp  :  I:fset(\mBbbN{})
{}\mrightarrow{}  i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
{}\mrightarrow{}  rho:X(I+i)
{}\mrightarrow{}  phi:\mBbbF{}(I)
{}\mrightarrow{}  u:\{I+i,s(phi)  \mvdash{}  \_:(A)<rho>  o  iota\}
{}\mrightarrow{}  cubical-path-0(X;A;I;i;rho;phi;u)
{}\mrightarrow{}  cubical-path-1(X;A;I;i;rho;phi;u)
8.  composition-uniformity(X;A;comp)
9.  I  :  fset(\mBbbN{})
10.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
11.  rho  :  Z(I+i)
12.  phi  :  \mBbbF{}(I)
13.  u  :  \{I+i,s(phi)  \mvdash{}  \_:((A)s2  o  s1)<rho>  o  iota\}
14.  x  :  cubical-path-0(Z;(A)s2  o  s1;I;i;rho;phi;u)
\mvdash{}  (comp  I  i  (s2)(s1)rho  phi  u  x)  =  (comp  I  i  (s2  o  s1)rho  phi  u  x)


By

---

Latex:
SubsumeC  \mkleeneopen{}cubical-path-1(X;A;I;i;(s2  o  s1)rho;phi;u)\mkleeneclose{}\mcdot{}

---

Home Index