---

Step * 1 of Lemma universe-comp-op-encode


1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. cT : X ⊢ CompOp(T)
4. encode(T;cT) ∈ {X ⊢ _:c𝕌}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : X(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(T)<rho> o iota}
10. a0 : cubical-path-0(X;T;I;i;rho;phi;u)
⊢ (compOp(encode(T;cT)) I i rho phi u a0) = (cT I i rho phi u a0) ∈ T((i1)(rho))
BY
{ (RepUR ``universe-encode universe-comp-op cubical-term-at csm-composition context-map functor-arrow csm-ap`` 0
   THEN Fold `cube-set-restriction` 0
   ) }

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. cT : X ⊢ CompOp(T)
4. encode(T;cT) ∈ {X ⊢ _:c𝕌}
5. I : fset(ℕ)
6. i : {i:ℕ| ¬i ∈ I} 
7. rho : X(I+i)
8. phi : 𝔽(I)
9. u : {I+i,s(phi) ⊢ _:(T)<rho> o iota}
10. a0 : cubical-path-0(X;T;I;i;rho;phi;u)
⊢ (cT I i 1(rho) phi u a0) = (cT I i rho phi u a0) ∈ T((i1)(rho))

---

Latex:

---

Latex:

1.  X  :  CubicalSet\{j\}
2.  T  :  \{X  \mvdash{}  \_\}
3.  cT  :  X  \mvdash{}  CompOp(T)
4.  encode(T;cT)  \mmember{}  \{X  \mvdash{}  \_:c\mBbbU{}\}
5.  I  :  fset(\mBbbN{})
6.  i  :  \{i:\mBbbN{}|  \mneg{}i  \mmember{}  I\} 
7.  rho  :  X(I+i)
8.  phi  :  \mBbbF{}(I)
9.  u  :  \{I+i,s(phi)  \mvdash{}  \_:(T)<rho>  o  iota\}
10.  a0  :  cubical-path-0(X;T;I;i;rho;phi;u)
\mvdash{}  (compOp(encode(T;cT))  I  i  rho  phi  u  a0)  =  (cT  I  i  rho  phi  u  a0)


By

---

Latex:
(...
  THEN  Fold  `cube-set-restriction`  0
  )

---

Home Index