---

Step * of Lemma universe-decode-type

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[rho:X(I)].  (decode((t)<rho>) = universe-type(t;I;rho) ∈ {formal-cube(I) ⊢ _})
BY
{ ((Intros⋅ THEN Symmetry)
   THEN (RWO "csm-universe-decode<" 0 THENA Auto)
   THEN (BLemma `cubical-type-equal2` THENA Auto)) }

1
1. X : CubicalSet{j}
2. t : {X ⊢ _:c𝕌}
3. I : fset(ℕ)
4. rho : X(I)
⊢ universe-type(t;I;rho)
= (decode(t))<rho>
∈ (A:I1:fset(ℕ) ⟶ formal-cube(I)(I1) ⟶ Type × (I1:fset(ℕ)
                                                ⟶ J:fset(ℕ)
                                                ⟶ f:J ⟶ I1
                                                ⟶ a:formal-cube(I)(I1)
                                                ⟶ (A I1 a)
                                                ⟶ (A J f(a))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[t:\{X  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:X(I)].    (decode((t)<rho>)  =  universe-type(t;I;rho))


By

---

Latex:
((Intros\mcdot{}  THEN  Symmetry)
  THEN  (RWO  "csm-universe-decode<"  0  THENA  Auto)
  THEN  (BLemma  `cubical-type-equal2`  THENA  Auto))

---

Home Index