---

Step * of Lemma can-apply-p-lift

∀[A,B:Type]. ∀[P:A ⟶ ℙ].  ∀d:x:A ⟶ Dec(P[x]). ∀f:{x:A| P[x]}  ⟶ B. ∀x:A.  (↑can-apply(p-lift(d;f);x) ⇐⇒ P[x])
BY
{ (RepUR ``can-apply p-lift`` 0 THEN (UnivCD THENA Auto)) }

1
1. [A] : Type
2. [B] : Type
3. [P] : A ⟶ ℙ
4. d : x:A ⟶ Dec(P[x])@i
5. f : {x:A| P[x]}  ⟶ B@i
6. x : A@i
⊢ ↑isl(case d x of inl(a) => inl (f x) | inr(a) => inr a ) ⇐⇒ P[x]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}d:x:A  {}\mrightarrow{}  Dec(P[x]).  \mforall{}f:\{x:A|  P[x]\}    {}\mrightarrow{}  B.  \mforall{}x:A.    (\muparrow{}can-apply(p-lift(d;f);x)  \mLeftarrow{}{}\mRightarrow{}  P[x])


By

---

Latex:
(RepUR  ``can-apply  p-lift``  0  THEN  (UnivCD  THENA  Auto))

---

Home Index