---

Step * of Lemma cubical-term-subtype-cubical-subset

∀[I:fset(ℕ)]. ∀[psi:𝔽(I)]. ∀[T:{formal-cube(I) ⊢ _}].  ({formal-cube(I) ⊢ _:T} ⊆r {I,psi ⊢ _:T})
BY
{ (Intros THEN (D 0 THENA Auto) THEN DVar `x' THEN MemTypeCD) }

1
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
⊢ x ∈ I@0:fset(ℕ) ⟶ a:I,psi(I@0) ⟶ T(a)

2
.....set predicate..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
⊢ ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I,psi(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))

3
.....wf..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. T : {formal-cube(I) ⊢ _}
4. x : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ T(a)
5. ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((x I@0 a a f) = (x J f(a)) ∈ T(f(a)))
6. u : I@0:fset(ℕ) ⟶ a:I,psi(I@0) ⟶ T(a)
⊢ ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:I,psi(I@0).  ((u I@0 a a f) = (u J f(a)) ∈ T(f(a))) ∈ Type

---

Latex:

---

Latex:
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].  \mforall{}[T:\{formal-cube(I)  \mvdash{}  \_\}].    (\{formal-cube(I)  \mvdash{}  \_:T\}  \msubseteq{}r  \{I,psi  \mvdash{}  \_:T\})


By

---

Latex:
(Intros  THEN  (D  0  THENA  Auto)  THEN  DVar  `x'  THEN  MemTypeCD)

---

Home Index