---

Step * of Lemma cube-_wf

No Annotations
∀[I:fset(ℕ)]. ∀[i:ℕ].  (cube-(I;i) ∈ formal-cube(I+i) j⟶ formal-cube(I).𝕀)
BY
{ (Intros THEN MemTypeCD) }

1
1. I : fset(ℕ)
2. i : ℕ
⊢ cube-(I;i) ∈ A:cat-ob(op-cat(CubeCat)) ⟶ (cat-arrow(type-cat{j':l}) (formal-cube(I+i) A) (formal-cube(I).𝕀 A))

2
.....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)))

3
.....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))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:fset(\mBbbN{})].  \mforall{}[i:\mBbbN{}].    (cube-(I;i)  \mmember{}  formal-cube(I+i)  j{}\mrightarrow{}  formal-cube(I).\mBbbI{})


By

---

Latex:
(Intros  THEN  MemTypeCD)

---

Home Index