---

Step * of Lemma psc-predicate_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[P:I:cat-ob(C) ⟶ X(I) ⟶ ℙ{[i | j']}].
  (psc-predicate(C; X; I,rho.P[I;rho]) ∈ ℙ{[i | j']})
BY
{ (Intros THEN Unfold `psc-predicate` 0) }

1
1. [C] : SmallCategory
2. [X] : ps_context{j:l}(C)
3. [P] : I:cat-ob(C) ⟶ X(I) ⟶ ℙ{[i | j']}
⊢ stable-element-predicate(C;X;I,rho.P[I;rho]) ∈ ℙ{[i | j']}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[P:I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}\{[i  |  j']\}].
    (psc-predicate(C;  X;  I,rho.P[I;rho])  \mmember{}  \mBbbP{}\{[i  |  j']\})


By

---

Latex:
(Intros  THEN  Unfold  `psc-predicate`  0)

---

Home Index