---

Step * of Lemma psc-adjoin-wf

No Annotations
∀[C:SmallCategory]. ∀[Gamma:ps_context{j:l}(C)]. ∀[A:{Gamma ⊢' _}].  (Gamma.A ∈ ps_context{[i | j]:l}(C))
BY
{ (Auto
   THEN MemContext
   THEN Try (Complete (Auto))
   THEN (Assert ∀I:cat-ob(C). (alpha:Gamma(I) × A(alpha) ∈ 𝕌{[i' | j']}) BY
               Auto)) }

1
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)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[Gamma:ps\_context\{j:l\}(C)].  \mforall{}[A:\{Gamma  \mvdash{}'  \_\}].
    (Gamma.A  \mmember{}  ps\_context\{[i  |  j]:l\}(C))


By

---

Latex:
(Auto
  THEN  MemContext
  THEN  Try  (Complete  (Auto))
  THEN  (Assert  \mforall{}I:cat-ob(C).  (alpha:Gamma(I)  \mtimes{}  A(alpha)  \mmember{}  \mBbbU{}\{[i'  |  j']\})  BY
                          Auto))

---

Home Index