---

Step * 1 of Lemma formal-cube-singleton1


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))
BY
{ ((Subst' f ⋅ g x ~ dM-lift(B;A;g) (f x) 0 THENA (RepUR ``nh-comp dM-lift dma-lift-compose`` 0 THEN Fold `dM` 0))
   THEN Auto
   ) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
2.  \mBbbI{}  \mmember{}  Functor(op-cat(CubeCat);TypeCat')
3.  A  :  fset(\mBbbN{})
4.  B  :  fset(\mBbbN{})
5.  g  :  names(A)  {}\mrightarrow{}  Point(dM(B))
6.  f  :  names(\{x\})  {}\mrightarrow{}  Point(dM(A))
\mvdash{}  (dM-lift(B;A;g)  (f  x))  =  (f  \mcdot{}  g  x)


By

---

Latex:
((Subst'  f  \mcdot{}  g  x  \msim{}  dM-lift(B;A;g)  (f  x)  0
    THENA  (RepUR  ``nh-comp  dM-lift  dma-lift-compose``  0  THEN  Fold  `dM`  0)
    )
  THEN  Auto
  )

---

Home Index