---

Step * of Lemma fpf-trivial-subtype-set

∀[A:Type]. ∀[P:A ─→ ℙ]. ∀[f:a:{a:A| P[a]}  fp-> Type × Top].  (f ∈ a:A fp-> Type × Top)
BY
{ (BasicUniformUnivCD Auto THEN At ⌈𝕌'⌉ (D 0)⋅ THEN Try (FpfSubtype)) }

1
.....wf..... 
1. A : Type
2. P : A ─→ ℙ
⊢ a:{a:A| P[a]}  fp-> Type × Top ∈ 𝕌'

---

Latex:


\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:a:\{a:A|  P[a]\}    fp->  Type  \mtimes{}  Top].    (f  \mmember{}  a:A  fp->  Type  \mtimes{}  Top)


By

(BasicUniformUnivCD  Auto  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Try  (FpfSubtype))

---

Home Index