---

Step * of Lemma cube-context-adjoin-I_cube

∀[Gamma,A,I:Top].  (Gamma.A(I) ~ alpha:Gamma(I) × A(alpha))
BY
{ PresheafMLTTInstance Obid: psc-adjoin-I_set⋅ }

---

Latex:

---

Latex:
\mforall{}[Gamma,A,I:Top].    (Gamma.A(I)  \msim{}  alpha:Gamma(I)  \mtimes{}  A(alpha))


By

---

Latex:
PresheafMLTTInstance  Obid:  psc-adjoin-I\_set\mcdot{}

---

Home Index