On Sunday 19 April 2009 9:31:27 pm Derek Elkins wrote:
simply because this is essentially a function with type
(forall a. F a) -> (exists a. F a)
and you can do that by instantiating the argument to any type, and then hiding it in an existential),
You can do this by using undefined, but without using undefined what if F a = Void ?
If it is, then you're giving me a Void, and I'm putting it in a box. Apparently I've not installed Agda since I installed GHC 6.10.2, but I'd expect something like the following to work: data VoidF (t : Set) : Set where data Unit : Set where unit : Unit data ∃ (f : Set -> Set) : Set1 where box : {t : Set} -> f t -> ∃ f box-it : (forall t -> VoidF t) -> ∃ VoidF box-it void = box (void Unit) It's just going to be difficult to get a value with type forall t -> VoidF t in the first place. -- Dan