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

[Nicolas Pouillard]

On Fri, 15 Oct 2010 11:55:54 +0200, Thorsten Altenkirch <txa at Cs.Nott.AC.UK> wrote:
> 
> On 15 Oct 2010, at 09:12, Andreas Abel wrote:
> 
> > 
> > On Oct 14, 2010, at 10:42 PM, Oscar Finnsson wrote:
> >>    There is no way to define False using records.
> >> 
> >> Why not? Something to do with type theory (from now on I'll just refer to type theory whenever I don't understand something :) )? If defining True using record is such a good idea why isn't defining False using record a good idea?
> >> ___________
> > 
> > False needs to be an empty type.  For instance the data type with no constructors.  A record type has by definition exactly one constructor.  Even if a record type has no fields, it is not empty.  It is then the nullary cartesian product, or the unit type, with exactly one inhabitant.
> > 
> > Of course you can define an empty record type if you already have an empty type "Empty".
> > 
> > record EmptyRec : Set where
> >  field
> >    bla : Empty
> > 
> > This, obviously, does not provide you with the first empty type who ever wandered on earth.
> 
> but we can use EmptyRec :-)
> 
> module emptyRec where
> 
> record EmptyRec : Set where
>  field
>    bla : EmptyRec
> 
> Recursive records forever!

elim-EmptyRec : ∀ {A : Set} → EmptyRec → A
elim-EmptyRec x = ?

-- 
Nicolas Pouillard
http://nicolaspouillard.fr