---

Step * of Lemma csm-cubical-subset-type-lemma

No Annotations
∀[Gamma,Delta:j⊢]. ∀[sigma:Delta j⟶ Gamma]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[i:{i:ℕ| ¬i ∈ I} ]. ∀[rho:Delta(I+i)].
∀[J:fset(ℕ)]. ∀[f:J ⟶ I].
  (((A)sigma(f((i1)(rho))) = A(f((i1)((sigma)rho))) ∈ Type) ∧ ((A)sigma(f((i0)(rho))) = A(f((i0)((sigma)rho))) ∈ Type))
BY
{ Auto }

---

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{}[J:fset(\mBbbN{})].  \mforall{}[f:J  {}\mrightarrow{}  I].
    (((A)sigma(f((i1)(rho)))  =  A(f((i1)((sigma)rho))))
    \mwedge{}  ((A)sigma(f((i0)(rho)))  =  A(f((i0)((sigma)rho)))))


By

---

Latex:
Auto

---

Home Index