---

Step * of Lemma universe-decode-encode

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

1
1. X : CubicalSet{j}
2. T : {X ⊢ _}
3. cT : X ⊢ CompOp(T)
4. encode(T;cT) ∈ {X ⊢ _:c𝕌}
⊢ decode(encode(T;cT))
= T
∈ (A:I:fset(ℕ) ⟶ X(I) ⟶ Type × (I:fset(ℕ) ⟶ J:fset(ℕ) ⟶ f:J ⟶ I ⟶ a:X(I) ⟶ (A I a) ⟶ (A J f(a))))

---

Latex:

---

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


By

---

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

---

Home Index