---

Step * 1 of Lemma csm-cubical-path-0-subtype

.....subterm..... T:t
1:n
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Delta(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. x : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
⊢ x ∈ cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)
BY
{ Assert ⌜{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}⌝⋅ }

1
.....assertion..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Delta(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. x : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
⊢ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}

2
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Delta(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. x : cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
11. {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}
⊢ x ∈ cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Gamma  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  sigma  :  Delta  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  I  :  fset(\mBbbN{})
6.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
7.  rho  :  Delta(I+i)
8.  phi  :  \mBbbF{}(I)
9.  u  :  \{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}
10.  x  :  cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)
\mvdash{}  x  \mmember{}  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)


By

---

Latex:
Assert  \mkleeneopen{}\{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}  =  \{I+i,s(phi)  \mvdash{}  \_:(A)<(sigma)rho>  o  iota\}\mkleeneclose{}\mcdot{}

---

Home Index