---

Step * 1 of Lemma univalence_wf


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

1
.....subterm..... T:t
1:n
1. G : CubicalSet{j}
⊢ G j⊢

2
.....subterm..... T:t
2:n
1. G : CubicalSet{j}
⊢ G ⊢' c𝕌

3
.....subterm..... T:t
3:n
1. G : CubicalSet{j}
⊢ G.c𝕌 ⊢' Contractible(Σ c𝕌 Equiv(decode((q)p);decode(q)))

---

Latex:

---

Latex:

1.  [G]  :  CubicalSet\{j\}
\mvdash{}  G  \mvdash{}'  \mPi{}c\mBbbU{}  Contractible(\mSigma{}  c\mBbbU{}  Equiv(decode((q)p);decode(q)))


By

---

Latex:
MemCD

---

Home Index