---

Step * 1 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)
⊢ (cT I i 1(rho) phi u a0) = (cT I i rho phi u a0) ∈ T((i1)(rho))
BY
{ RepeatFor 4 (EqCDA) }

1
.....subterm..... T:t
2:n
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)
⊢ 1(rho) = rho ∈ X(I+i)

---

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{}  (cT  I  i  1(rho)  phi  u  a0)  =  (cT  I  i  rho  phi  u  a0)


By

---

Latex:
RepeatFor  4  (EqCDA)

---

Home Index