---

Step * 2 of Lemma cubical-subset-term

.....set predicate..... 
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)]
⊢ ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I).  ((t I a a f) = (t J f(a)) ∈ {t:T | ∀I,alpha. psi[I;alpha;t]}(f(a)))
BY
{ (Auto THEN RepUR ``cubical-subset`` 0 THEN Symmetry THEN EqTypeCD THEN Auto THEN Fold `cubical-term-at` 0 THEN Auto) }

---

Latex:

---

Latex:
.....set  predicate..... 
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)]
\mvdash{}  \mforall{}I,J:fset(\mBbbN{}).  \mforall{}f:J  {}\mrightarrow{}  I.  \mforall{}a:X(I).    ((t  I  a  a  f)  =  (t  J  f(a)))


By

---

Latex:
(Auto
  THEN  RepUR  ``cubical-subset``  0
  THEN  Symmetry
  THEN  EqTypeCD
  THEN  Auto
  THEN  Fold  `cubical-term-at`  0
  THEN  Auto)

---

Home Index