Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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

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




Archive powered by MHonArc 2.6.18.

Top of Page