---

Step * 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)]
⊢ t ∈ I:fset(ℕ) ⟶ a:X(I) ⟶ {t:T | ∀I,alpha. psi[I;alpha;t]}(a)
BY
{ (RepeatFor 2 ((FunExt THENA Auto))
   THEN Fold `cubical-term-at` 0
   THEN RepUR ``cubical-subset`` 0
   THEN MemTypeCD
   THEN Auto) }

1
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}

---

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)]
\mvdash{}  t  \mmember{}  I:fset(\mBbbN{})  {}\mrightarrow{}  a:X(I)  {}\mrightarrow{}  \{t:T  |  \mforall{}I,alpha.  psi[I;alpha;t]\}(a)


By

---

Latex:
(RepeatFor  2  ((FunExt  THENA  Auto))
  THEN  Fold  `cubical-term-at`  0
  THEN  RepUR  ``cubical-subset``  0
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index