Hi Thorsten I'm not sure I understand what's going on here.

Thorsten Altenkirch wrote:

Indeed, in the setoid model we can construct a function f : A -> [B] ------------------ lift f : [A -> B]if the setoid A is "trivial", i.e. has the identity as its equivalencerelation.

I can do it if A is decided. If you give me a : A, then I pick lift f = iI const (f a) Ii or, in less idiomatic longhand lift f = do c <- return const b <- f a return (c b) If you give me A -> 0, it's easy.

f : A -> B/~ --------------------- lift f : (A -> B)/~'

Again, if you give me some a : A, I say

`lift f = const (f a) -- const respects the equivalence because const`

`b a ~' const b' a if b ~ b'`

But hang on - what stops us from doing a Diaconescu? Excluded middledoesn't hold in the setoid model, even though we only get P \/ not Pwhere A \/ B = [A + B]. But this would still require that we have P +not P in the underlying set. So what goes wrong?We define the type of non-empty subsets of Bool as NE = Sigma Q : Bool-> Prop.Sigma x:Bool.Q x

Note that NE is inhabited, eg by moo = (const 1; true; ()).

We define the equivalence relation of extensional equality of subsets ~ : NE -> NE -> Prop (Q,_) ~ (R,_) = forall b:Bool.Q b <-> R b Now we derive: h : NE/~ -> [ NE ]which is just the indentity on the underlying elements. The point isthat obviously ~ implies the trivial equality of [..].Now, if we were able to lift h we get lift h : [ NE/~ -> NE]

return (const moo) : [ NE/~ -> NE]

Obviously, NE/~ isn't a setoid with a trivial equality! The Diaconescu argument shows that we can prove for any P:Prop H : NE/~ -> NE ---------------------- Dia H : P \/ not P = [P + not P]

Dia (const moo) : P \/ not P

see below for a Epigram 2+n style proof of Dia.

Under the circumstances, I really hope you've cocked this up.

We can also see what goes wrong in general: The principle f : A -> B/~ --------------------- lift f : (A -> B)/~'fails because given the setoid A = (A0,~A) the premise gives us anunderlying function f0:A0 -> B (for simplicity we assume that B istrivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the samefunction to construct an element of A -> B we need to show that a ~Ab implies f0 a = f0 b, and there is no reason to believe this - unless~A is the equality.

`I just about swallow that. But if A0 is decided, you need to use the`

`spec part (which you're eliding for simplicity) to force me to use f0 in`

`the way you're suggesting.`

P.S.For completeness: Dia itself can be constructed as in the COQ script:we useT,F : Bool -> PropT b = (b=true) \/ P F b = (b=false) \/ Pby applying H to the equivalence classe <T>,<F> and projecting out thecomponents we gett,f : Bool t = fst (H <T>) f = fst (H <F>) snd (H <T>) : t=true \/ P snd (H <F>) : f=false \/ P

Are you sure? I thought H had return type NE, giving (P; a; p) = fst (H <T>), (Q, b, q) := fst(H <F>) : Bool -> Prop where a,b : Bool, p : P a, q : Q b but no connection necessary between T and P, F and Q.

`Now, I know that my pathological functions are not the functions you're`

`thinking of, but it does rather show that the real action, whatever it`

`is, lies in the "spec" parts which you're throwing away.`

More later Conor PS I blogged a bit about implementing OTT...