---

Step * 1 1 1 1 1 1 of Lemma cubical-interval-filler-fills


1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : cubical-interval()(I-[v])
⊢ (v:=v1)(v@0) = v@0 ∈ cubical-interval()(I-[v])
BY
{ (RepUR ``cubical-interval I-cube functor-ob`` -1
   THEN RepUR ``cube-set-restriction cubical-interval I-cube functor-ob`` 0
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN EqCD
   THEN Auto
   THEN (BLemma `name-morph-ext` THENA Auto)) }

1
1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : name-morph(I-[v];[]) ⟶ ℕ2
5. x : name-morph(I-[v];[])
⊢ (v:=v1) ∈ name-morph(I-[v];I-[v])

2
1. I : Cname List
2. v : nameset(I)
3. v1 : ℕ2
4. v@0 : name-morph(I-[v];[]) ⟶ ℕ2
5. x : name-morph(I-[v];[])
⊢ ∀x1:nameset(I-[v]). ((((v:=v1) o x) x1) = (x x1) ∈ extd-nameset([]))

---

Latex:

---

Latex:

1.  I  :  Cname  List
2.  v  :  nameset(I)
3.  v1  :  \mBbbN{}2
4.  v@0  :  cubical-interval()(I-[v])
\mvdash{}  (v:=v1)(v@0)  =  v@0


By

---

Latex:
(RepUR  ``cubical-interval  I-cube  functor-ob``  -1
  THEN  RepUR  ``cube-set-restriction  cubical-interval  I-cube  functor-ob``  0
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto
  THEN  (BLemma  `name-morph-ext`  THENA  Auto))

---

Home Index