---

Step * of Lemma cubical-subset_wf

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[psi:I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ].
  X ⊢ {t:T | ∀I,alpha. psi[I;alpha;t]} supposing cubical-type-restriction(X;T;I,a,t.psi[I;a;t])
BY
{ (Unfold `cubical-type-restriction` 0 THEN Intros) }

1
1. [X] : CubicalSet{j}
2. [T] : {X ⊢ _}
3. [psi] : I:fset(ℕ) ⟶ alpha:X(I) ⟶ T(alpha) ⟶ ℙ
4. [%] : ∀I,J:fset(ℕ). ∀f:J ⟶ I. ∀a:X(I). ∀t:T(a).  (psi[I;a;t] ⇒ psi[J;f(a);(t a f)])
⊢ X ⊢ {t:T | ∀I,alpha. psi[I;alpha;t]}

---

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{}].
    X  \mvdash{}  \{t:T  |  \mforall{}I,alpha.  psi[I;alpha;t]\}  supposing  cubical-type-restriction(X;T;I,a,t.psi[I;a;t])


By

---

Latex:
(Unfold  `cubical-type-restriction`  0  THEN  Intros)

---

Home Index