---

Step * of Lemma cubical-equiv-p

No Annotations
∀[H:j⊢]. ∀[T,A,E:{H ⊢ _}].  ((Equiv(A;E))p = Equiv((A)p;(E)p) ∈ {H.T ⊢ _})
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H:j\mvdash{}].  \mforall{}[T,A,E:\{H  \mvdash{}  \_\}].    ((Equiv(A;E))p  =  Equiv((A)p;(E)p))


By

---

Latex:
Auto

---

Home Index