[Agda] wishlist/some help wanted

[Tristan Wibberley]

On Sun, 2008-04-27 at 01:07 +0100, Nils Anders Danielsson wrote:
> On Sat, Apr 26, 2008 at 10:31 PM, Tristan Wibberley
> <tristan at wibberley.org> wrote:
> 

> >  4) It seems that sometimes for some proof object "p" proving a predicate
> >  "P", when "P => Q", "p" is also a proof object of "Q", yet other times
> >  it isn't.
> 
> I don't follow you here. Can you give an example?

For example, boolean or: a proof object of "(a || b) istrue" is also a
proof object of "(b || a) istrue". But in other cases a proof object of
one is not of the other - although I don't have an example to hand.

Above || is the boolean or, "true istrue" is an empty record and "false
istrue" is an empty data.

I'm using predicates like:

dosomething : (n : Nat) -> {_ : Q n} -> Nat
...

fn : (n : Nat) -> {_ : P n} -> Nat
fn (satisfies_P n) {p} = dosomething n {p}
fn (doesnt_satisfy_P n) {}

here I'm using p as a proof object of both P and Q, and, depending on P
and Q, this will work sometimes and at other times needs:

fn (satisfies_P n) {p} = dosomething n {proof_P_impl_Q n p}

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.