---

Step * of Lemma formal-cube-singleton1

∀x:ℕ. (λA,f. (f x) ∈ 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 RepUR ``compose names-hom`` 0
   THEN FunExt
   THEN Reduce 0
   THEN Auto
   THEN RenameVar `f' (-1)) }

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

---

Latex:

---

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


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  RepUR  ``compose  names-hom``  0
  THEN  FunExt
  THEN  Reduce  0
  THEN  Auto
  THEN  RenameVar  `f'  (-1))

---

Home Index