---

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


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. [u1] : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)
11. [u2] : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
12. [%1] : u1 = u2 ∈ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
13. ∀[u:{I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota}]. (cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u) ∈ 𝕌{[i' | j']})
⊢ cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)
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. u1 : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)
11. u2 : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
12. u1 = u2 ∈ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
13. ∀[u:{I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota}]. (cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u) ∈ 𝕌{[i' | j']})
⊢ {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. [u1] : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
10. cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)
11. [u2] : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
12. [%1] : u1 = u2 ∈ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
13. ∀[u:{I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota}]. (cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u) ∈ 𝕌{[i' | j']})
14. {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}
⊢ cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)

---

Latex:

---

Latex:

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.  [u1]  :  \{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}
10.  cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1)  \msubseteq{}r  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)
11.  [u2]  :  \{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}
12.  [\%1]  :  u1  =  u2
13.  \mforall{}[u:\{I+i,s(phi)  \mvdash{}  \_:(A)<(sigma)rho>  o  iota\}]
            (cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u)  \mmember{}  \mBbbU{}\{[i'  |  j']\})
\mvdash{}  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)  \msubseteq{}r  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)


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