coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simplest example of impredicative Prop?

From: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>
To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
Cc: Bas Spitters <spitters AT cs.ru.nl>, coq-club AT inria.fr
Subject: Re: [Coq-Club] Simplest example of impredicative Prop?
Date: Tue, 31 Jul 2012 11:07:01 -0400

Very interesting. Just to check: this is saying that we need a universe *instead of* impredicative Prop for this example?

- B

On Jul 31, 2012, at 3:16 AM, Arnaud Spiwack wrote:

Mmm, very clever.

My bad then. I'll have to retract my example.

On 30 July 2012 15:40, Bas Spitters <spitters AT cs.ru.nl> wrote:

> surjectivity is equivalent to being epi in the category of setoids

You need at least a universe to prove this statement:
http://www2.math.uu.se/research/pub/Wilander2.pdf

but if you have a universe the statement can be proved.

Bas

[Coq-Club] Simplest example of impredicative Prop?, Benjamin C. Pierce, 07/25/2012
- Re: [Coq-Club] Simplest example of impredicative Prop?, Adam Chlipala, 07/25/2012
- Re: [Coq-Club] Simplest example of impredicative Prop?, gallais @ ensl.org, 07/25/2012
- Re: [Coq-Club] Simplest example of impredicative Prop?, Chung-Kil Hur, 07/25/2012
- Re: [Coq-Club] Simplest example of impredicative Prop?, Arnaud Spiwack, 07/27/2012
  - Re: [Coq-Club] Simplest example of impredicative Prop?, Bas Spitters, 07/30/2012
    - Re: [Coq-Club] Simplest example of impredicative Prop?, Arnaud Spiwack, 07/31/2012
      - Re: [Coq-Club] Simplest example of impredicative Prop?, Benjamin C. Pierce, 07/31/2012
        
        Re: [Coq-Club] Simplest example of impredicative Prop?, Arnaud Spiwack, 07/31/2012