Library bar

Require Import prelude.
Require Import hlemmas.


Section hpropEM.

  Variable explicit_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) ×
                    (forall a, (r a = f a) + (g (r a) = a)).

  Variable A : Type.
  Variable Aprop : hprop A.

  Definition f : nat + (A + ¬ A) -> nat :=
    fun x => match x with
              inl n => S n
            | inr _ => 0
             end.

  Definition g : nat -> nat + (A + ¬ A) := fun x => inl x.

  Lemma injective_f : injective f.
   unfold f; intros [?|[?|?]] [?|[?|?]]; intros; try congruence.
   - repeat apply f_equal. apply Aprop.
   - repeat apply f_equal. apply neg_hprop.
  Qed.

  Lemma injective_g : injective g.
   unfold g; intros ? ? ?.
   injection H; auto.
  Qed.

  Lemma EMA_nat_hset : hset (nat + (A + ¬ A)).
    apply plus_hset.
    - apply nat_hset.
    - apply plus_hset; apply hprop_hset; [assumption|apply neg_hprop].
  Qed.

  Definition rtuple := explicit_hset_CB _ _ g f nat_hset EMA_nat_hset injective_g injective_f.

  Definition r := π₁ rtuple.
  Definition r_inv := let (a, _) := π₂ rtuple in π₁ a.
  Definition iso : inverse r r_inv.
    unfold r_inv,r.
    destruct rtuple; simpl.
    destruct p.
    destruct s.
    exact i.
  Defined.

  Definition cond : forall a, (r a = g a) + (f (r a) = a).
    unfold r; destruct rtuple as [? [? u]]; exact u.
  Defined.

End hpropEM.