Hi Conor,
I'm not sure I understand what's going on here.
This happens if you don't type check your definitions. I got carried
away with my non-dependent simplification of the story.
Thank you for actually reading it.
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
equivalence relation.
I can do it if A is decided. If you give me a : A, then I pick
lift f = iI const (f a) Ii
Indeed, however your trick won't work for the dependent version:
f : Pi a:A.[B a]
---------------------
lift f: [Pi a:A.B a]
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'
Dito. We need
f : Pi a:A.(B a)/(~ a)
-------------------------
lift f: (Pi a:A.B a)/~'
where ~' is defined as before: f ~' g = Pi a:A.f a ~ g a but for
f,g : Pi a:A.B a and ~ is actually a family of equivalence relations
~' : Pi a:A.(B a) -> (B a) -> Prop.
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 ]
We define
h0 : Pi (P,_):NE . [ Sigma b:2.P b ]
h0 (P,p) = return p
and observe that this trivially preserves ~ and hence we obtain
h : Pi (P,_):NE/~ . [ Sigma b:2.P b ]
Now, if we were able to lift h we get
lift h : [ NE/~ -> NE]
return (const moo) : [ NE/~ -> NE]
lift h : [ Pi (P,_):NE/~ . Sigma b:2.P b ]
and your version ceases to work.
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]
Corrected:
H : Pi (P,_):NE/~ . Sigma b:2.P b
--------------------------------------------
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.
I have.
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 an
underlying function f0:A0 -> B (for simplicity we assume that B is
trivial) s.t. a ~A b implies f0 a ~B f0 b, where to use the same
function to construct an element of A -> B we need to show that
a ~A b 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.
You are right. The reasoning only works for the dependent version.
P.S.
For completeness: Dia itself can be constructed as in the COQ
script: we use
T,F : Bool -> Prop
T b = (b=true) \/ P
F b = (b=false) \/ P
by applying H to the equivalence classe <T>,<F> and projecting out
the components we get
t,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.
This should now work with the correct type of H.
Cheers,
Thorsten
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
