[Agda] Status of Prop

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi Conor,

is not extensionality for singleton types missing here to make your
example work?

> data TT : Prop where
>   tt : TT
>
> moo : TT -> Set
> moo tt = Nat
>
> boo : {x : TT} -> moo x
> boo = zero -- goes wrong

If you have eta for TT, then you know that x is definitionally equal to
tt, and then moo x = Nat, definitionally.

Cheers,
Andreas

Conor McBride wrote:
> Hi Ulf
> 
> I'm guessing this is a known problem, and one source of
> "experimental status", but...
> 
> On 2 Sep 2008, at 08:08, Ulf Norell wrote:
> 
>>
>> Prop is experimental at the moment. The rules are
>>
>> Prop < Set
>> Prop : Set1
>>
>> A : Set   P : Prop
>> -----------------------
>> (x : A) -> P : Prop
>>
>> There's a flag --proof-irrelevance which makes Prop proof irrelevant,
>> but also ensures that
>> propositions have at most one element by restricting datatypes in Prop
>> to have at most one
>> constructor.
> 
> Having at most one value is necessary but not sufficient
> for proof irrelevance. You also need a certain laziness.
> Here's why
> 
> -------------------------------------------------
> {-# OPTIONS --proof-irrelevance #-}
> 
> module PI where
> 
> data TT : Prop where
>   tt : TT
> 
> data Nat : Set where
>   zero : Nat
>   suc : Nat -> Nat
> 
> moo : TT -> Set
> moo tt = Nat
> 
> yay : {x : TT} -> moo tt
> yay = zero -- works fine
> 
> boo : {x : TT} -> moo x
> boo = zero -- goes wrong
> ---------------------------------------------------
> 
> In the traditional Orwellian style, all TT's are equal,
> but some are more equal than others.
> 
> All the best
> 
> Conor
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 


- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFIwOl4PMHaDxpUpLMRAlBKAKC5AEMDYo3f0ARPSciPubghpTQ1ngCZAVPN
Oqsg9HikQcAbVsyjb5li8cM=
=0ICU
-----END PGP SIGNATURE-----