The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I don't immediately see any way around using functional extensionality
and propositional extensionality in the proof.  You could maybe
restrict the propositional extensionality to the special case: forall
P:Prop, P -> P = True.  Or, as you somewhat hinted at, if you assume
classic_dec : forall P:Prop, {P} + {~P}, then you can use Z := bool,
g1 := fun y => sumbool_to_bool (classic_dec (y ∈ im f)), g2 := fun y
=> true.

On the other hand, if you change the category definition to make the
Hom spaces into setoids, then you should be able to adapt this proof
to show that epimorphisms in the category of setoids are surjective,
axiom free.
-- 
Daniel Schepler

On Fri, Aug 8, 2014 at 9:30 AM, John Wiegley 
<jwiegley AT gmail.com>
 wrote:
>>>>>> Adam Chlipala 
>>>>>> <adamc AT csail.mit.edu>
>>>>>>  writes:
>
>> I suggest reading the lemma statement more carefully.  IMO, it's clearly
>> false even in common intuitive interpretations, and Coq agrees.
>
> You're right, I forgot to include the premise that P a is in fact provable.
>
> Given that, and with propositional equality, the proof goes through.  But 
> I'm
> uneasy with that axiom, so let me describe the context in which it came up:
> I'm trying to prove that epic functions are exactly the surjective functions
> in the category of sets (see below).
>
> Most informal proofs on the web prove this by contradiction, which I do not
> think helps me in a constructive setting?  One web page mentions using a
> "characteristic function" from Y → {0,1}, although I couldn't figure out how
> to encode that.  Clearly the trick lies in picking the right g1 and g2
> functions when specializing my hypothesis.
>
> The full development is here (and yes, it is in sore need of good, 
> Adam-style
> proof scripting!):
>
>     https://github.com/jwiegley/category-theory/blob/master/Products.v#L150
>
> Thanks,
>   John
>
> ------------------------------------------------------------------------
>
>   Program Instance Sets : Category :=
>   { ob      := Type
>   ; hom     := fun X Y => X → Y
>   ; id      := fun _ x => x
>   ; compose := fun _ _ _ f g x => f (g x)
>   }.
>
>   Section EpisMonos.
>
>     Context `{C : Category}.
>     Variable X Y : C.
>     Variable f : X ~{C}~> Y.
>
>     Definition Epic := ∀ {Z} (g1 g2 : Y ~> Z), g1 ∘ f = g2 ∘ f → g1 = g2.
>
>   End EpisMonos.
>
>   Lemma existence_exists :
>     ∀ {A} (a : A) (P : A → Prop), P a → (∃ y : A, P y) = P a.
>   Proof.
>     intros.
>     assert (forall P Q : Prop, P <-> Q -> P = Q).
>       intros. destruct H0. admit.
>     apply H0.
>     split; intros; auto.
>     exists a.
>     assumption.
>   Qed.
>
>   Lemma surjectivity_is_epic `(f : X ~> Y)
>     : (∀ y, ∃ x, f x = y) ↔ @Epic Sets X Y f.
>   Proof. split.
>   - intros.
>     unfold Epic.
>     intros.
>     simpl in H0.
>     extensionality e.
>     specialize (H e).
>     destruct H.
>     rewrite <- H.
>     apply (equal_f H0).
>   - intros.
>     unfold Epic in H.
>     specialize H with (Z := Prop).
>     specialize H with (g1 := fun y0 => ∃ x0, f x0 = y0).
>     simpl in *.
>     specialize H with (g2 := fun y  => y = y).
>     eapply equal_f in H.
>     erewrite H. constructor.
>     extensionality e.
>     rewrite (existence_exists e).
>     reflexivity.
>     reflexivity.
>   Qed.