---

Step * of Lemma cubical-subset-term

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[psi:I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ].
  ∀[t:{X ⊢ _:T}]
    t ∈ {X ⊢ _:{t:T | ∀I,alpha. psi[I;alpha;t]}} supposing ∀I:fset(ℕ). ∀alpha:X(I).  psi[I;alpha;t(alpha)] 
  supposing cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
BY
{ (Intros THEN Unhide THEN DVar `t' THEN (MemTypeCD THENW 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)]
⊢ t ∈ I:fset(ℕ) ⟶ a:X(I) ⟶ {t:T | ∀I,alpha. psi[I;alpha;t]}(a)

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[psi:I:fset(\mBbbN{})  {}\mrightarrow{}  alpha:X(I)  {}\mrightarrow{}  T(alpha)  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}[t:\{X  \mvdash{}  \_:T\}]
        t  \mmember{}  \{X  \mvdash{}  \_:\{t:T  |  \mforall{}I,alpha.  psi[I;alpha;t]\}\} 
        supposing  \mforall{}I:fset(\mBbbN{}).  \mforall{}alpha:X(I).    psi[I;alpha;t(alpha)] 
    supposing  cubical-type-restriction(X;T;I,a,t.psi[I;a;t])


By

---

Latex:
(Intros  THEN  Unhide  THEN  DVar  `t'  THEN  (MemTypeCD  THENW  Auto))

---

Home Index