---

Step * of Lemma formal-cube-singleton2

∀x:ℕ. (λA,u,x. u ∈ nat-trans(op-cat(CubeCat);TypeCat';𝕀;formal-cube({x})))
BY
{ (Intro
   THEN (Assert 𝕀 ∈ Functor(op-cat(CubeCat);TypeCat') BY
               ((Fold `ps_context` 0 THEN Fold `cubical_set` 0) THEN Auto))
   THEN (BLemma `is-nat-trans` THENW Auto)
   THEN RepUR ``op-cat  cube-cat type-cat interval-presheaf formal-cube`` 0
   THEN RepUR ``compose names-hom`` 0
   THEN Auto
   THEN (FunExt THENW Auto)
   THEN Reduce 0
   THEN RenameVar `u' (-1)) }

1
1. x : ℕ
2. 𝕀 ∈ Functor(op-cat(CubeCat);TypeCat')
3. A : fset(ℕ)
4. B : fset(ℕ)
5. g : names(A) ⟶ Point(dM(B))
6. u : Point(dM(A))
⊢ λx@0.u ⋅ g = (λx@0.(dM-lift(B;A;g) u)) ∈ (names({x}) ⟶ Point(dM(B)))

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}.  (\mlambda{}A,u,x.  u  \mmember{}  nat-trans(op-cat(CubeCat);TypeCat';\mBbbI{};formal-cube(\{x\})))


By

---

Latex:
(Intro
  THEN  (Assert  \mBbbI{}  \mmember{}  Functor(op-cat(CubeCat);TypeCat')  BY
                          ((Fold  `ps\_context`  0  THEN  Fold  `cubical\_set`  0)  THEN  Auto))
  THEN  (BLemma  `is-nat-trans`  THENW  Auto)
  THEN  RepUR  ``op-cat    cube-cat  type-cat  interval-presheaf  formal-cube``  0
  THEN  RepUR  ``compose  names-hom``  0
  THEN  Auto
  THEN  (FunExt  THENW  Auto)
  THEN  Reduce  0
  THEN  RenameVar  `u'  (-1))

---

Home Index