---

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

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Delta(I+i)].
∀[phi:𝔽(I)]. ∀[u1,u2:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}].
  cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2) 
  supposing u1 = u2 ∈ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
BY
{ (InstLemma `csm-cubical-path-0-subtype` []
   THEN RepeatFor 9 (ParallelLast')
   THEN Intros
   THEN (Enough to prove cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)
          Because (SubtypeTrans (-4) (-1) THEN 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}
⊢ 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:
No  Annotations
\mforall{}[Gamma,Delta:j\mvdash{}].  \mforall{}[sigma:Delta  j{}\mrightarrow{}  Gamma].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\}  ].
\mforall{}[rho:Delta(I+i)].  \mforall{}[phi:\mBbbF{}(I)].  \mforall{}[u1,u2:\{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}].
    cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u1)  \msubseteq{}r  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2) 
    supposing  u1  =  u2


By

---

Latex:
(InstLemma  `csm-cubical-path-0-subtype`  []
  THEN  RepeatFor  9  (ParallelLast')
  THEN  Intros
  THEN  (Enough  to  prove  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u1)
                                                  \msubseteq{}r  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u2)
                Because  (SubtypeTrans  (-4)  (-1)  THEN  Auto)))

---

Home Index