---

Step * 1 of Lemma psc-fst_wf


1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. A : {Gamma ⊢ _}
4. I : cat-ob(C)
5. p : Gamma.A(I)
⊢ p ∈ Gamma(I) × Top
BY
{ (RepUR ``psc-adjoin`` -1 THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  A  :  \{Gamma  \mvdash{}  \_\}
4.  I  :  cat-ob(C)
5.  p  :  Gamma.A(I)
\mvdash{}  p  \mmember{}  Gamma(I)  \mtimes{}  Top


By

---

Latex:
(RepUR  ``psc-adjoin``  -1  THEN  Auto)

---

Home Index