Commit f929abf3 authored by Nicola Botta's avatar Nicola Botta
Browse files

Initial.

parent 83219b4b
module issues.CannotSolveConstraint3
Surjective : {s, t : Type} -> (f : s -> t) -> Type
Surjective {s} {t} f = (y : t) -> DPair s (\ x => f x = y)
NonSurjective : {s, t : Type} -> (f : s -> t) -> Type
NonSurjective {s} {t} f = DPair t (\ y => (x : s) -> Not (f x = y))
nonSurjectiveNotSurjective : {s, t : Type} -> (f : s -> t) -> NonSurjective f -> Not (Surjective f)
nonSurjectiveNotSurjective f (MkDPair y faxnfxy) =
-- \ surjectivef => let x = fst (surjectivef y) in (faxnfxy x) (snd (surjectivef y))
\ surjectivef => (faxnfxy (fst (surjectivef y))) (snd (surjectivef y))
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment