---

Step * of Lemma universe-comp-op-encode

No Annotations
∀[X:j⊢]. ∀[T:{X ⊢ _}]. ∀[cT:X ⊢ CompOp(T)].  (compOp(encode(T;cT)) = cT ∈ X ⊢ CompOp(T))
BY
{ (Intros
   THEN (Assert encode(T;cT) ∈ {X ⊢ _:c𝕌} BY
               Auto)
   THEN (BLemma `equal-composition-op2` THENA Auto)
   THEN Intros) }

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)
⊢ (compOp(encode(T;cT)) I i rho phi u a0) = (cT I i rho phi u a0) ∈ T((i1)(rho))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{X  \mvdash{}  \_\}].  \mforall{}[cT:X  \mvdash{}  CompOp(T)].    (compOp(encode(T;cT))  =  cT)


By

---

Latex:
(Intros
  THEN  (Assert  encode(T;cT)  \mmember{}  \{X  \mvdash{}  \_:c\mBbbU{}\}  BY
                          Auto)
  THEN  (BLemma  `equal-composition-op2`  THENA  Auto)
  THEN  Intros)

---

Home Index