---

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

No Annotations
∀[I:fset(ℕ)]. ∀[psi:𝔽(I)].  (I,psi = formal-cube(I), λJ,f. f(psi) ∈ CubicalSet{j})
BY
{ ((Intros THEN (InstLemma `formal-cube_wf` [⌜parm{j}⌝;⌜I⌝]⋅ THENA Auto))
   THEN InstLemma `cubical_sets_equal` [⌜parm{j}⌝]⋅
   THEN BHyp -1) }

1
.....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)))
⊢ I,psi j⊢

2
.....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)))
⊢ formal-cube(I), λJ,f. f(psi) j⊢

3
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,psi = formal-cube(I), λJ,f. f(psi) ∈ (F:fset(ℕ) ⟶ 𝕌{j'} × (x:fset(ℕ) ⟶ y:fset(ℕ) ⟶ y ⟶ x ⟶ (F x) ⟶ (F y)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[psi:\mBbbF{}(I)].    (I,psi  =  formal-cube(I),  \mlambda{}J,f.  f(psi))


By

---

Latex:
((Intros  THEN  (InstLemma  `formal-cube\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  InstLemma  `cubical\_sets\_equal`  [\mkleeneopen{}parm\{j\}\mkleeneclose{}]\mcdot{}
  THEN  BHyp  -1)

---

Home Index