---

Step * 2 1 of Lemma cubical-subset-is-context-subset


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ λJ,f. f(psi) ∈ {formal-cube(I) ⊢ _:𝔽}
BY
{ MemTypeCD }

1
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ λJ,f. f(psi) ∈ I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ 𝔽(a)

2
.....set predicate..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
⊢ ∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  (((λJ,f. f(psi)) I@0 a a f) = ((λJ,f. f(psi)) J f(a)) ∈ 𝔽(f(a)))

3
.....wf..... 
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. formal-cube(I) j⊢
4. ∀[X,Y:j⊢].
     X = Y ∈ CubicalSet{j} supposing X = Y ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))
5. u : I@0:fset(ℕ) ⟶ a:formal-cube(I)(I@0) ⟶ 𝔽(a)
⊢ istype(∀I@0,J:fset(ℕ). ∀f:J ⟶ I@0. ∀a:formal-cube(I)(I@0).  ((u I@0 a a f) = (u J f(a)) ∈ 𝔽(f(a))))

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  formal-cube(I)  j\mvdash{}
4.  \mforall{}[X,Y:j\mvdash{}].    X  =  Y  supposing  X  =  Y
\mvdash{}  \mlambda{}J,f.  f(psi)  \mmember{}  \{formal-cube(I)  \mvdash{}  \_:\mBbbF{}\}


By

---

Latex:
MemTypeCD

---

Home Index