---

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


1. I : fset(ℕ)
2. psi : 𝔽(I)
3. I,psi = formal-cube(I), λJ,f. f(psi) ∈ CubicalSet{j}
4. formal-cube(I) j⊢
⊢ canonical-section(();𝔽;I;⋅;psi) = (λJ,f. f(psi)) ∈ (I1:fset(ℕ) ⟶ a:formal-cube(I)(I1) ⟶ 𝔽(a))
BY
{ ((FunExt THENA Auto)
   THEN RenameVar `J' (-1)
   THEN (FunExt THENA Auto)
   THEN RepUR ``formal-cube`` -1
   THEN RepUR ``canonical-section`` 0) }

1
1. I : fset(ℕ)
2. psi : 𝔽(I)
3. I,psi = formal-cube(I), λJ,f. f(psi) ∈ CubicalSet{j}
4. formal-cube(I) j⊢
5. J : fset(ℕ)
6. a : J ⟶ I
⊢ (psi ⋅ a) = a(psi) ∈ 𝔽(a)

---

Latex:

---

Latex:

1.  I  :  fset(\mBbbN{})
2.  psi  :  \mBbbF{}(I)
3.  I,psi  =  formal-cube(I),  \mlambda{}J,f.  f(psi)
4.  formal-cube(I)  j\mvdash{}
\mvdash{}  canonical-section(();\mBbbF{};I;\mcdot{};psi)  =  (\mlambda{}J,f.  f(psi))


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  RenameVar  `J'  (-1)
  THEN  (FunExt  THENA  Auto)
  THEN  RepUR  ``formal-cube``  -1
  THEN  RepUR  ``canonical-section``  0)

---

Home Index