---

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

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Delta(I+i)].
∀[phi:𝔽(I)]. ∀[u:{I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}].
  (cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u) ⊆r cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u))
BY
{ (Auto THEN (D 0 THENA Auto)) }

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

---

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{}[u:\{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}].
    (cubical-path-0(Delta;(A)sigma;I;i;rho;phi;u)  \msubseteq{}r  cubical-path-0(Gamma;A;I;i;(sigma)rho;phi;u))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto))

---

Home Index