---

Step * 2 of Lemma cube-_wf

.....set predicate..... 
1. I : fset(ℕ)
2. i : ℕ
⊢ ∀A,B:cat-ob(op-cat(CubeCat)). ∀g:cat-arrow(op-cat(CubeCat)) A B.
    ((cat-comp(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 A) (formal-cube(I).𝕀 B) (cube-(I;i) A) 
      (formal-cube(I).𝕀 A B g))
    = (cat-comp(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I+i) B) (formal-cube(I).𝕀 B) (formal-cube(I+i) A B g) 
       (cube-(I;i) B))
    ∈ (cat-arrow(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 B)))
BY
{ (RepUR ``cat-ob op-cat names-cat cat-arrow type-cat functor-ob formal-cube`` 0
   THEN RepUR ``cube-context-adjoin functor-arrow cat-comp compose`` 0
   THEN (RWO "interval-type-at" 0 THENA Auto)
   THEN RepUR ``interval-presheaf cube-`` 0
   THEN Intros
   THEN (FunExt THENA Auto)
   THEN Reduce 0
   THEN EqCD) }

1
.....subterm..... T:t
1:n
1. I : fset(ℕ)
2. i : ℕ
3. A : fset(ℕ)
4. B : fset(ℕ)
5. g : B ⟶ A
6. x : A ⟶ I+i
⊢ x ⋅ g = x ⋅ g ∈ B ⟶ I

2
.....subterm..... T:t
2:n
1. I : fset(ℕ)
2. i : ℕ
3. A : fset(ℕ)
4. B : fset(ℕ)
5. g : B ⟶ A
6. x : A ⟶ I+i
⊢ (x i x g) = (x ⋅ g i) ∈ Point(dM(B))

3
.....eq aux..... 
1. I : fset(ℕ)
2. i : ℕ
3. A : fset(ℕ)
4. B : fset(ℕ)
5. g : B ⟶ A
6. x : A ⟶ I+i
7. alpha : B ⟶ I
⊢ istype(Point(dM(B)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
\mvdash{}  \mforall{}A,B:cat-ob(op-cat(CubeCat)).  \mforall{}g:cat-arrow(op-cat(CubeCat))  A  B.
        ((cat-comp(type-cat\{j':l\})  (formal-cube(I+i)  A)  (formal-cube(I).\mBbbI{}  A)  (formal-cube(I).\mBbbI{}  B) 
            (cube-(I;i)  A) 
            (formal-cube(I).\mBbbI{}  A  B  g))
        =  (cat-comp(type-cat\{j':l\})  (formal-cube(I+i)  A)  (formal-cube(I+i)  B)  (formal-cube(I).\mBbbI{}  B) 
              (formal-cube(I+i)  A  B  g) 
              (cube-(I;i)  B)))


By

---

Latex:
(RepUR  ``cat-ob  op-cat  names-cat  cat-arrow  type-cat  functor-ob  formal-cube``  0
  THEN  RepUR  ``cube-context-adjoin  functor-arrow  cat-comp  compose``  0
  THEN  (RWO  "interval-type-at"  0  THENA  Auto)
  THEN  RepUR  ``interval-presheaf  cube-``  0
  THEN  Intros
  THEN  (FunExt  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD)

---

Home Index