[Agda] Status of Prop

[Conor McBride]

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