The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  Haha, nice that you found the place I'm using it. That svn add should never had happened! I'm not sure the proof can be fixed, and there's been much work since then on formalizing categories that I would recommend you read instead of my poor man's, naive and as you can see bug ridden attempt at it.

  Anyhow, in the section functor proof I probably must show that two (hom a b)'s are Leibniz equal but I can't and instead show that they're just extensionally, i.e. pointwise Leibniz, equal. So maybe this could just resort to the functional extensionality axiom instead of the obviously wrong setoid_ext. I'm on a smartphone and couldn't check though.

Best,
-- Matthieu

Le mardi 7 janvier 2014, Daniil Frumin a écrit :

Thanks a lot, this is easy indeed. I just got confused by the supposed
use of it in Matthieu's code: http://mattam.org/repos/coq/cat/TYPE.v

I wonder if it is possible to fix that proof at all?

On Tue, Jan 7, 2014 at 9:04 PM, Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr> wrote:
> It's fairly blatant indeed. The proof of inconsistency is almost a one-liner
> (I omitted the equivalence relation requirement for pedagogical purposes,
> but it is clear that R is indeed an equivalence relation):
>
>
> Axiom setoideq_eq : forall {A:Type} (R:A->A->Prop) (x y : A), R x y -> x =
> y.
>
> Goal False.
> Proof.
>   set (R := fun x y : bool => True).
>   generalize (setoideq_eq R true false I); intros h.
>   discriminate h.
> Qed.
>
>
> On 7 January 2014 17:46, Daniil Frumin <difrumin AT gmail.com> wrote:
>>
>> It used to state the following:
>>
>> Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
>>
>> Application of the extensionality principle for setoids.
>>
>> Ltac setoid_extensionality :=
>>   match goal with
>>     [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
>>   end.
>>
>> I am pretty much a newb, so I am not sure if that's blatantly inconsistent
>>
>> thanks
>>
>> On Tue, Jan 7, 2014 at 8:24 PM, Pierre-Marie Pédrot
>> <pierre-marie.pedrot AT inria.fr> wrote:
>> > On 07/01/2014 16:59, Daniil Frumin wrote:
>> >> It has disappeared in V8.3 and I didn't find the mention of it in the
>> >> changelog
>> >> and the last commit that removes it is
>> >> 3b5e12a2eb98b34cacc1850f63b702dfea26cd57
>> >>
>> >> In particular I am looking for setoid_extensionality.
>> >
>> > Wasn't that an inconsistent axiom? I think I remember it stated
>> > something plain wrong. Can you remind us its type?
>> >
>> > PMP
>> >
>>
>>
>>
>> --
>> Sincerely yours,
>> -- Daniil
>>
>



--
Sincerely yours,
-- Daniil

-- 
-- Matthieu