---

Step * 1 of Lemma psc-predicate_wf


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']}
BY
{ (Unfold `stable-element-predicate` 0
   THEN RepeatFor 3 ((MemCD THENL [Auto; Id]))
   THEN (MemCD
         THENL [((RepeatFor 2 (DVar `X') THEN All Reduce) THEN DoSubsume THEN Auto THEN RepUR ``type-cat`` 0 THEN Auto)
               ; Id]
   )) }

1
.....subterm..... T:t
2:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. P : I:cat-ob(C) ⟶ X(I) ⟶ ℙ{[i | j']}
4. I : cat-ob(C)
5. J : cat-ob(C)
6. f : cat-arrow(C) J I
7. rho : X I
⊢ P[I;rho] ⇒ P[J;X I J f rho] ∈ ℙ{[i | j']}

---

Latex:

---

Latex:

1.  [C]  :  SmallCategory
2.  [X]  :  ps\_context\{j:l\}(C)
3.  [P]  :  I:cat-ob(C)  {}\mrightarrow{}  X(I)  {}\mrightarrow{}  \mBbbP{}\{[i  |  j']\}
\mvdash{}  stable-element-predicate(C;X;I,rho.P[I;rho])  \mmember{}  \mBbbP{}\{[i  |  j']\}


By

---

Latex:
(Unfold  `stable-element-predicate`  0
  THEN  RepeatFor  3  ((MemCD  THENL  [Auto;  Id]))
  THEN  (MemCD
              THENL  [((RepeatFor  2  (DVar  `X')  THEN  All  Reduce)
                              THEN  DoSubsume
                              THEN  Auto
                              THEN  RepUR  ``type-cat``  0
                              THEN  Auto)
                          ;  Id]
  ))

---

Home Index