---

Step * of Lemma csm-swap_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _}].  (csm-swap(G;A;B) ∈ G.A.(B)p ij⟶ G.B.(A)p)
BY
{ PresheafMLTTInstance Obid: pscm-swap_wf⋅ }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_\}].    (csm-swap(G;A;B)  \mmember{}  G.A.(B)p  ij{}\mrightarrow{}  G.B.(A)p)


By

---

Latex:
PresheafMLTTInstance  Obid:  pscm-swap\_wf\mcdot{}

---

Home Index