[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Dan Doel]

On Tuesday 12 October 2010 8:00:36 pm Samuel Gélineau wrote:
> > 16. Why is False defined as
> > 
> > > data False : Set where
> > 
> > while True is defined as
> > 
> > > record True : Set where
> > 
> > and why aren't both using the same sort of definition (data or record)?
> 
> Because it's shorter and more symmetrical that way.

Actually, I suspect the reason (and it's the best one) is eta expansion. The 
record version has it, and the data version doesn't. And it means that all 
functions into True become definitionally equal:

   f, g : A -> True

   f
     = eta (functions)
   \x -> f x
     = eta (True)
   \x -> record {}
     = eta (True)
   \x -> g x
     = eta (functions)
   g

It even works on \() : False -> True. This can't even be proved for the data 
version (unless I'm missing something) without extensionality.

-- Dan