---

Step * 1 of Lemma formal-cube-singleton2


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)))
BY
{ ((FunExt THENA Auto) THEN Reduce 0 THEN RepUR ``names`` -1 THEN D -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))
7. x1 : ℕ
8. x1 ∈ {x}
⊢ (λx@0.u ⋅ g x1) = (dM-lift(B;A;g) u) ∈ Point(dM(B))

---

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.  u  :  Point(dM(A))
\mvdash{}  \mlambda{}x@0.u  \mcdot{}  g  =  (\mlambda{}x@0.(dM-lift(B;A;g)  u))


By

---

Latex:
((FunExt  THENA  Auto)  THEN  Reduce  0  THEN  RepUR  ``names``  -1  THEN  D  -1)

---

Home Index