Replace the proof that epi and surjective are the same with the one using mapping cones and truncation

[JasonGross]

As per HoTT/coq#120 (comment), the current proof that epi + mono -> iso in the category of sets only goes through by exploiting a bug in the universe level algorithm (which is now fixed in trunk). Using the mapping cone/truncation proof should fix this.

[spitters]

I was not exploiting a bug, I just choose a slightly different than you
did. Both make sense.
For compatibility the mapping cone proof seems better.

On Thu, Jun 26, 2014 at 10:41 PM, Jason Gross [email protected]
wrote:

As per HoTT/coq#120 (comment)
HoTT/coq#120 (comment), the
current proof that epi + mono -> iso in the category of sets only goes
through by exploiting a bug in the universe level algorithm (which is now
fixed in trunk). Using the mapping cone/truncation proof should fix this.

—
Reply to this email directly or view it on GitHub
#404.

[JasonGross]

You were not exploiting a bug, but I was. I reported the bug as "this definition goes through, but I get a universe inconsistency if I inline this 'let'". It turned out that the reason was that the 'let' made Coq forget about some universe constraints, and without that, it doesn't go through. If I understand your discussion with Matthieu correctly, the only ways to make my theorem in Functor/Attributes go through are to use the mapping cone proof for epi and surjective, or to have an impredicative hprop.

[spitters]

Ah OK.

Yes, those seem to be basically the two options.

On Thu, Jun 26, 2014 at 11:06 PM, Jason Gross [email protected]
wrote:

You were not exploiting a bug, but I was. I reported the bug as "this
definition goes through, but I get a universe inconsistency if I inline
this 'let'". It turned out that the reason was that the 'let' made Coq
forget about some universe constraints, and without that, it doesn't go
through. If I understand your discussion with Matthieu correctly, the only
ways to make my theorem in Functor/Attributes go through are to use the
mapping cone proof for epi and surjective, or to have an impredicative
hprop.

—
Reply to this email directly or view it on GitHub
#404 (comment).

[mattam82]

I'm working on formalizing that proof using the mapping cone now.

Le jeudi 26 juin 2014, Bas Spitters [email protected] a écrit :

Ah OK.

Yes, those seem to be basically the two options.

On Thu, Jun 26, 2014 at 11:06 PM, Jason Gross <[email protected]
javascript:_e(%7B%7D,'cvml','[email protected]');>
wrote:

You were not exploiting a bug, but I was. I reported the bug as "this
definition goes through, but I get a universe inconsistency if I inline
this 'let'". It turned out that the reason was that the 'let' made Coq
forget about some universe constraints, and without that, it doesn't go
through. If I understand your discussion with Matthieu correctly, the
only
ways to make my theorem in Functor/Attributes go through are to use the
mapping cone proof for epi and surjective, or to have an impredicative
hprop.

—
Reply to this email directly or view it on GitHub
#404 (comment).

—
Reply to this email directly or view it on GitHub
#404 (comment).

[mattam82]

It turns out to be quite easy using the Truncations to finish it, so I have it now in my fork. Attributes goes through with this.

[spitters]

@mattam82 Sorry, what is Attributes? One of @JasonGross files?

On Wed, Jul 2, 2014 at 10:52 AM, Matthieu Sozeau [email protected]
wrote:

It turns out to be quite easy using the Truncations to finish it, so I
have it now in my fork. Attributes goes through with this.

—
Reply to this email directly or view it on GitHub
#404 (comment).

[mattam82]

Yes, the one that required the unification with an epi proof where all X Y Z are at the same level.