Library topem

Require Import prelude.
Require Import ninfty.
Require Import hlemmas.

Lemma crucial : forall (A : Type) (O : Type), omniscient O ->
                 forall (f : O + A -> O) g, section_retraction f g ->
                 A + ¬ A.
  intros.
  destruct (X (fun o => match g o with
                         inl _ => false
                       | inr _ => true
                        end)).
  + left; destruct s as [x ?]; case_eq (g x); intros.
    - rewrite H0 in e; inversion e.
    - assumption.
  + right; intros a.
    specialize (e (f (inr a))); rewrite H in e; inversion e.
Qed.

Section PEM.

  Variable hset_CB :
    forall (A B : Type) (f : A -> B) (g : B -> A),
      hset A -> hset B -> injective f -> injective g -> Σ (r : A -> B), (Σ r_inv, inverse r r_inv).

  Variable A : Type.
  Variable Aprop : hprop A.

  Theorem PEM : A + ¬ A.
    pose (f := fun x => match (x : _ + A) with
                         inl k => succ_infty k
                       | inr _ => zero_infty
                        end).
    pose (g := @inl ℕ∞ A).
    assert (injective g) by (intros ? ? H; injection H; congruence).
    assert (injective f).
    {
      intros ? ? ?.
      destruct a, a'; subst f; simpl in *.
      + apply f_equal, injective_succ_infty, H0.
      + exfalso; eapply noconf_infty; eassumption.
      + exfalso; eapply noconf_infty; eauto.
      + apply f_equal, Aprop.
    }
    assert (hset (ℕ∞ + A)) by (apply plus_hset; [apply N_infty_hset|apply hprop_hset, Aprop]).
    destruct (hset_CB _ _ f g H1 N_infty_hset H0 H) as [s [r [p q]]].
    eapply crucial; eauto.
    apply N_infty_omniscient.
  Qed.

End PEM.