daily pastebin goal
83%
SHARE
TWEET

Untitled

a guest Jun 13th, 2018 51 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. someLemma3 : {A : Set} {P : A → Set} {Q : A → Set} {B : Set} (f' : (∃ f ∈ (B → A) , (((b : B) → P (f b)) ∧ ((a : A) → P a → ((∃ b ∈ B , (f b == a))))))) → (((a : A) → P a → Q a) ↔ ((b : B) → Q ((π₁ f') b)))
  2.   someLemma3 {A} {P} {Q} {B} (f , (hyp-a , hyp-b)) = (proof-a , proof-b)
  3.    where
  4.     proof-a :  ((a : A) → P a → Q a) → (b : B) → Q (f b)
  5.     proof-a subhyp b = subhyp (f b) (hyp-a b)
  6.  
  7.     proof-b :  ((b : B) → Q (f b)) → (a : A) → P a → Q a
  8.     proof-b subhyp a Pa = ([A==B]→A→B ([x==y]→[fx==fy] Q {f (π₁ (hyp-b a Pa))} {a} (π₂ (hyp-b a Pa)))) (subhyp (π₁ (hyp-b a Pa)))
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top