---

Step * 1 of Lemma cube+_wf


1. [I] : fset(ℕ)
2. [i] : ℕ
⊢ cube+(I;i) ∈ formal-cube(I).𝕀 j⟶ formal-cube(I+i)
BY
{ 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).𝕀 A) (formal-cube(I+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).𝕀 A) (formal-cube(I+i) A) (formal-cube(I+i) B) (cube+(I;i) A) 
      (formal-cube(I+i) A B g))
    = (cat-comp(type-cat{j':l}) (formal-cube(I).𝕀 A) (formal-cube(I).𝕀 B) (formal-cube(I+i) B) (formal-cube(I).𝕀 A B g) 
       (cube+(I;i) B))
    ∈ (cat-arrow(type-cat{j':l}) (formal-cube(I).𝕀 A) (formal-cube(I+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).𝕀 A) (formal-cube(I+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).𝕀 A) (formal-cube(I+i) A) (formal-cube(I+i) B) (trans A) 
             (formal-cube(I+i) A B g))
           = (cat-comp(type-cat{j':l}) (formal-cube(I).𝕀 A) (formal-cube(I).𝕀 B) (formal-cube(I+i) B) 
              (formal-cube(I).𝕀 A B g) 
              (trans B))
           ∈ (cat-arrow(type-cat{j':l}) (formal-cube(I).𝕀 A) (formal-cube(I+i) B))))

---

Latex:

---

Latex:

1.  [I]  :  fset(\mBbbN{})
2.  [i]  :  \mBbbN{}
\mvdash{}  cube+(I;i)  \mmember{}  formal-cube(I).\mBbbI{}  j{}\mrightarrow{}  formal-cube(I+i)


By

---

Latex:
MemTypeCD

---

Home Index