---

Step * 1 of Lemma psc-adjoin-wf


1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. A : {Gamma ⊢' _}
4. ∀I:cat-ob(C). (alpha:Gamma(I) × A(alpha) ∈ 𝕌{[i' | j']})
⊢ ∀I:cat-ob(C). ∀s:alpha:Gamma(I) × A(alpha).
    (<cat-id(C) I(fst(s)), (snd(s) fst(s) cat-id(C) I)> = s ∈ (alpha:Gamma(I) × A(alpha)))
BY
{ (Auto THEN D -1 THEN Reduce 0 THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  A  :  \{Gamma  \mvdash{}'  \_\}
4.  \mforall{}I:cat-ob(C).  (alpha:Gamma(I)  \mtimes{}  A(alpha)  \mmember{}  \mBbbU{}\{[i'  |  j']\})
\mvdash{}  \mforall{}I:cat-ob(C).  \mforall{}s:alpha:Gamma(I)  \mtimes{}  A(alpha).
        (<cat-id(C)  I(fst(s)),  (snd(s)  fst(s)  cat-id(C)  I)>  =  s)


By

---

Latex:
(Auto  THEN  D  -1  THEN  Reduce  0  THEN  EqCDA  THEN  Auto)

---

Home Index