The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-28T01:48:07+09:00, Andrej Bauer wrote:

>>The construction in Blass's paper starts with a set Y = {u,v} of
>>cardinality 2.  For every proposition P, he defines an equivalence
>>relation R(P) on Y as follows:
>>
>> 1. (u,u) \in R(P)
>> 2. (v,v) \in R(P)
>> 3. P -> (u,v) \in R(P)
>> 4. P -> (v,u) \in R(P).
>
> This, strictly speaking, is not a definition. You might get one if you
> required R(P) to be the least equivalence relation satisfying the
> above 4 conditions.

Yes, that's true.  In my script, I actually defined it as

Inductive blass (P : Prop) : bool -> bool -> Prop :=
| b_0 : blass P true true
| b_1 : blass P false false
| b_2 : P -> blass P true false
| b_3 : P -> blass P false true.

> But it is much easier to define R(P) as
>
> R(P) = { (x,y) : Y x Y | x = y \/ P }.
>
> No need for any inductive stuff. Also, Y is just bool.

You mean like

Definition blass' (P : Prop) (x y : bool) : Prop :=
  x = y \/ P.

If so, yes, that looks much neater.

> In any case, it is probably useful to learn about setoids, but your
> proof will be, at the end of the day, essentially a proof of decequiv
> -> lem, but packaed up in the setoid technology.

As must be obvious, I am a beginner in Coq.  I'm reading Pierce's book
linearly, solving all the exercises.  So, if setoids aren't really going
to help me prove deceq -> lem, I'll postpone reading about them.

Regarding quotients, I was wondering if it is possible in Coq to work
with the functor that the quotient set represents instead of working
with the quotient set itself.

What I mean is that given a set Y and an equivalence relation R on Y, we
get a functor F(R) : Sets -> Sets which takes any set A to the set
F(R)(A) of all functions f : Y -> A which are R-invariant (i.e.,
constant on R-equivalence classes).  For every element y of Y, we get a
morphism of functors H(R)(y) : F(R) -> Id, where Id is the identity
functor Sets -> Sets.  For any set A, the map H(R)(y)(A) : F(R)(A) -> A
is defined by H(R)(y)(A)(f) = f(y).

If two elements y1 and y2 of Y are R-equivalent, then certainly

   H(R)(y1)(A)(f) = f(y1) = f(y2) = H(R)(y2)(A)(f),

hence H(R)(y1) = H(R)(y2).  Conversely, if H(R)(y1) = H(R)(y2), then
taking A to be the power set of Y, and f : Y -> A to be the function
which maps every element y of Y to its equivalence class R[y], we get

   R[y1] = f(y1) = H(R)(y1)(A)(f) = H(R)(y2)(A)(f) = f(y2) = R[y2],

hence y1 and y2 are R-equivalent.  Therefore, if X(R) is the "set" of
all morphisms of functors F(R) -> Id, then the function H(R) : Y -> X(R)
which maps y in Y to H(R)(y) separates exactly the R-inequivalent
elements.  That is, its fibres are precisely the R-equivalence classes
in Y.  So, X(R) could serve as a model for the quotient set Y / R.

I haven't checked the details, and it's possible I've gone over the deep
end here, but if not, and if there's something here that I can formalise
in Coq, that'd be good to know.

Thanks and best regards,
Raghu.

PS : Thanks for the videos!  They helped me start using Proof General.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/