---

Step * 1 of Lemma fpf-trivial-subtype-set

.....wf..... 
1. A : Type
2. P : A ─→ ℙ
⊢ a:{a:A| P[a]}  fp-> Type × Top ∈ 𝕌'
BY
{ (Unfold `fpf` 0 THEN Auto) }

---

Latex:


.....wf..... 
1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  a:\{a:A|  P[a]\}    fp->  Type  \mtimes{}  Top  \mmember{}  \mBbbU{}'


By

(Unfold  `fpf`  0  THEN  Auto)

---

Home Index