---

Step * 1 1 of Lemma csm-cubical-path-1-subtype

.....assertion..... 
1. Gamma : CubicalSet{j}
2. Delta : CubicalSet{j}
3. sigma : Delta j⟶ Gamma
4. A : {Gamma ⊢ _}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : Delta(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota}
⊢ {I+i,s(phi) ⊢ _:((A)sigma)<rho> o iota} = {I+i,s(phi) ⊢ _:(A)<(sigma)rho> o iota} ∈ 𝕌{[i' | j']}
BY
{ (EqCDA
   THEN (RWO "csm-ap-comp-type" 0 THENA Auto)
   THEN EqCDA
   THEN (RWO "csm-ap-comp-type<" 0 THENA Auto)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  Gamma  :  CubicalSet\{j\}
2.  Delta  :  CubicalSet\{j\}
3.  sigma  :  Delta  j{}\mrightarrow{}  Gamma
4.  A  :  \{Gamma  \mvdash{}  \_\}
5.  I  :  fset(\mBbbN{})
6.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
7.  rho  :  Delta(I+i)
8.  phi  :  \mBbbF{}(I)
9.  u  :  \{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}
\mvdash{}  \{I+i,s(phi)  \mvdash{}  \_:((A)sigma)<rho>  o  iota\}  =  \{I+i,s(phi)  \mvdash{}  \_:(A)<(sigma)rho>  o  iota\}


By

---

Latex:
(EqCDA
  THEN  (RWO  "csm-ap-comp-type"  0  THENA  Auto)
  THEN  EqCDA
  THEN  (RWO  "csm-ap-comp-type<"  0  THENA  Auto)
  THEN  EqCD
  THEN  Auto)

---

Home Index