---

Step * of Lemma interval-presheaf_wf

No Annotations
𝕀 ∈ SmallCubicalSet
BY
{ (Unfold `small_cubical_set` 0
   THEN ProveWfLemma
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto
   THEN All (RepUR ``cat-id cat-ob cat-arrow op-cat names-cat cat-comp type-cat``)
   THEN BLemma `dM-lift-unique-fun`
   THEN Try (QuickAuto)) }

1
.....wf..... 
1. x : fset(ℕ)
⊢ λx.x ∈ dma-hom(dM(x);dM(x))

2
.....wf..... 
1. ∀x:fset(ℕ). (dM-lift(x;x;1) = (λx.x) ∈ (Point(dM(x)) ⟶ Point(dM(x))))
2. x : fset(ℕ)
3. y : fset(ℕ)
4. z : fset(ℕ)
5. f : y ⟶ x
6. g : z ⟶ y
⊢ dM-lift(z;y;g) o dM-lift(y;x;f) ∈ dma-hom(dM(x);dM(z))

3
1. ∀x:fset(ℕ). (dM-lift(x;x;1) = (λx.x) ∈ (Point(dM(x)) ⟶ Point(dM(x))))
2. x : fset(ℕ)
3. y : fset(ℕ)
4. z : fset(ℕ)
5. f : y ⟶ x
6. g : z ⟶ y
⊢ ∀j:names(x). (((dM-lift(z;y;g) o dM-lift(y;x;f)) <j>) = (f ⋅ g j) ∈ Point(dM(z)))

---

Latex:

---

Latex:
No  Annotations
\mBbbI{}  \mmember{}  SmallCubicalSet


By

---

Latex:
(Unfold  `small\_cubical\_set`  0
  THEN  ProveWfLemma
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto
  THEN  All  (RepUR  ``cat-id  cat-ob  cat-arrow  op-cat  names-cat  cat-comp  type-cat``)
  THEN  BLemma  `dM-lift-unique-fun`
  THEN  Try  (QuickAuto))

---

Home Index