The Coq mailing list

["John Wiegley" <jwiegley AT gmail.com>]

>>>>> 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.