---

Step * of Lemma canonical-section_wf

No Annotations
∀[Gamma:j⊢]. ∀[A:{Gamma ⊢ _}]. ∀[I:fset(ℕ)]. ∀[rho:Gamma(I)]. ∀[a:A(rho)].
  (canonical-section(Gamma;A;I;rho;a) ∈ {formal-cube(I) ⊢ _:(A)<rho>})
BY
{ PresheafMLTTInstance Obid: ps-canonical-section_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[Gamma:j\mvdash{}].  \mforall{}[A:\{Gamma  \mvdash{}  \_\}].  \mforall{}[I:fset(\mBbbN{})].  \mforall{}[rho:Gamma(I)].  \mforall{}[a:A(rho)].
    (canonical-section(Gamma;A;I;rho;a)  \mmember{}  \{formal-cube(I)  \mvdash{}  \_:(A)<rho>\})


By

---

Latex:
PresheafMLTTInstance  Obid:  ps-canonical-section\_wf\mcdot{}

---

Home Index