---

Step * 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}
⊢ cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)
BY
{ (InstLemma `cubical-path-0_wf` [⌜Gamma⌝;⌜A⌝;⌜I⌝;⌜i⌝;⌜(sigma)rho⌝;⌜phi⌝]⋅ THENA Auto) }

1
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)

---

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
\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:
(InstLemma  `cubical-path-0\_wf`  [\mkleeneopen{}Gamma\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}(sigma)rho\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index