---

Step * of Lemma cc-adjoin-cube-restriction

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}]. ∀[J,K,g,v,u:Top].  (g((v;u)) ~ (g(v);(u v g)))
BY
{ PresheafMLTTInstance Obid: psc-adjoin-set-restriction⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[J,K,g,v,u:Top].    (g((v;u))  \msim{}  (g(v);(u  v  g)))


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-adjoin-set-restriction\mcdot{}

---

Home Index