---

Step * 3 of Lemma cube-_wf

.....wf..... 
1. I : fset(ℕ)
2. i : ℕ
3. trans : A:cat-ob(op-cat(CubeCat)) ⟶ (cat-arrow(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 A))
⊢ istype(∀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) (trans 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) 
              (trans B))
           ∈ (cat-arrow(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 B))))
BY
{ (MoveToConcl (-1) 
   THEN Fold `I_cube` 0
   THEN RepUR ``type-cat compose`` 0
   THEN Unfold `functor-arrow` 0
   THEN Fold `cube-set-restriction` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  fset(\mBbbN{})
2.  i  :  \mBbbN{}
3.  trans  :  A:cat-ob(op-cat(CubeCat))  {}\mrightarrow{}  (cat-arrow(type-cat\{j':l\})  (formal-cube(I+i)  A) 
                                                                                  (formal-cube(I).\mBbbI{}  A))
\mvdash{}  istype(\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) 
                          (trans  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) 
                            (trans  B))))


By

---

Latex:
(MoveToConcl  (-1) 
  THEN  Fold  `I\_cube`  0
  THEN  RepUR  ``type-cat  compose``  0
  THEN  Unfold  `functor-arrow`  0
  THEN  Fold  `cube-set-restriction`  0
  THEN  Auto)

---

Home Index