---

Step * of Lemma univalence_wf

No Annotations
∀[G:j⊢]. G ⊢' Univalence
BY
{ (Intros THEN Unfold `univalence` 0) }

1
1. [G] : CubicalSet{j}
⊢ G ⊢' Πc𝕌 Contractible(Σ c𝕌 Equiv(decode((q)p);decode(q)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  G  \mvdash{}'  Univalence


By

---

Latex:
(Intros  THEN  Unfold  `univalence`  0)

---

Home Index