---

Step * of Lemma csm+_wf

No Annotations
∀[H,K:j⊢]. ∀[A:{H ⊢ _}]. ∀[tau:K j⟶ H].  (tau+ ∈ K.(A)tau ij⟶ H.A)
BY
{ PresheafMLTTInstance Obid: pscm+_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[H,K:j\mvdash{}].  \mforall{}[A:\{H  \mvdash{}  \_\}].  \mforall{}[tau:K  j{}\mrightarrow{}  H].    (tau+  \mmember{}  K.(A)tau  ij{}\mrightarrow{}  H.A)


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm+\_wf\mcdot{}

---

Home Index