---

Step * of Lemma universe-type-at

No Annotations
∀[X:j⊢]. ∀[t:{X ⊢ _:c𝕌}]. ∀[I:fset(ℕ)]. ∀[a:X(I)]. ∀[K:fset(ℕ)]. ∀[f:K ⟶ I].
  (universe-type(t;I;a)(f) = decode(t)(f(a)) ∈ Type)
BY
{ (Intros⋅
   THEN (RWO "universe-decode-type<" 0 THENA Auto)
   THEN RWW "csm-universe-decode< csm-ap-type-at csm-ap-context-map" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros\mcdot{}
  THEN  (RWO  "universe-decode-type<"  0  THENA  Auto)
  THEN  RWW  "csm-universe-decode<  csm-ap-type-at  csm-ap-context-map"  0
  THEN  Auto)

---

Home Index