---

Step * 1 1 of Lemma cubical-subset-term


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. psi : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
5. t : I:fset(ℕ) ⟶ a:X(I) ⟶ T(a)
6. ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((t I a a f) = (t J f(a)) ∈ T(f(a)))
7. ∀I:fset(ℕ). ∀alpha:X(I).  psi[I;alpha;t(alpha)]
8. I : fset(ℕ)
9. a : X(I)
⊢ t ∈ {X ⊢ _:T}
BY
{ (MemTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  psi  :  I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  \mBbbP{}
4.  cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
5.  t  :  I:fset(\mBbbN{})  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  T(a)
6.  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:X(I).    ((t  I  a  a  f)  =  (t  J  f(a)))
7.  \mforall{}I:fset(\mBbbN{}).  \mforall{}alpha:X(I).    psi[I;alpha;t(alpha)]
8.  I  :  fset(\mBbbN{})
9.  a  :  X(I)
\mvdash{}  t  \mmember{}  \{X  \mvdash{}  \_:T\}


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index