Library misc.projective

Require Import HoTT HitTactics.
Require Import subobjects.k_finite subobjects.b_finite FSets.
Require Import misc.dec_lem.

Class IsProjective (X : Type) :=
  projective : ∀ {P Q : Type} (p : P → Q) (f : X → Q),
      IsSurjection p → hexists (fun (g : X → P) ⇒ p o g = f).

Instance IsProjective_IsHProp `{Univalence} X : IsHProp (IsProjective X).
Proof. unfold IsProjective. apply _. Defined.

Instance Unit_Projective `{Univalence} : IsProjective Unit.
Proof.
  intros P Q p f Hsurj.
  pose (x' := center (merely (hfiber p (f tt)))).
  simple refine (@Trunc_rec (-1) (hfiber p (f tt)) _ _ _ x'). clear x'; intro x.
  simple refine (tr (fun _ ⇒ x.1;_)). simpl.
  apply path_forall; intros [].
  apply x.2.
Defined.

Instance Empty_Projective `{Univalence} : IsProjective Empty.
Proof.
  intros P Q p f Hsurj.
  apply tr. ∃ Empty_rec.
  apply path_forall. intros [].
Defined.

Instance Sum_Projective `{Univalence} {A B: Type} `{IsProjective A} `{IsProjective B} :
  IsProjective (A + B).
Proof.
  intros P Q p f Hsurj.
  pose (f1 := fun a ⇒ f (inl a)).
  pose (f2 := fun b ⇒ f (inr b)).
  pose (g1' := projective p f1 Hsurj).
  pose (g2' := projective p f2 Hsurj).
  simple refine (Trunc_rec _ g1') ; intros [g1 pg1].
  simple refine (Trunc_rec _ g2') ; intros [g2 pg2].
  simple refine (tr (_;_)).
  - intros [a | b].
    + apply (g1 a).
    + apply (g2 b).
  - apply path_forall; intros [a | b]; simpl.
    + apply (ap (fun h ⇒ h a) pg1).
    + apply (ap (fun h ⇒ h b) pg2).
Defined.

Section b_fin_projective.
  Context `{Univalence}.

  Global Instance bishop_projective (X : Type) (Hfin : Finite X) : IsProjective X.
  Proof.
    simple refine (finite_ind_hprop (fun X _ ⇒ IsProjective X) _ _ X);
      simpl; apply _.
  Defined.
End b_fin_projective.

Section k_fin_lemoo_projective.
  Context `{Univalence}.
  Context {LEMoo : ∀ (P : Type), Decidable P}.
  Global Instance kuratowski_projective_oo (X : Type) (Hfin : Kf X) : IsProjective X.
  Proof.
    assert (Finite X).
    { eapply Kf_to_Bf; auto.
      intros pp qq. apply LEMoo. }
    apply _.
  Defined.
End k_fin_lemoo_projective.

Section k_fin_lem_projective.
  Context `{Univalence}.
  Context {LEM : ∀ (P : Type) {Hprop : IsHProp P}, Decidable P}.
  Variable (X : Type).
  Context `{IsHSet X}.

  Global Instance kuratowski_projective (Hfin : Kf X) : IsProjective X.
  Proof.
    assert (Finite X).
    { eapply Kf_to_Bf; auto.
      intros pp qq. apply LEM. apply _. }
    apply _.
  Defined.
End k_fin_lem_projective.

Section k_fin_projective_lem.
  Context `{Univalence}.
  Variable (P : Type).
  Context `{IsHProp P}.

  Definition X : Type := TR (BuildhProp P).
  Instance X_set : IsHSet X.
  Proof.
    apply _.
  Defined.

  Definition X_fin : Kf X.
  Proof.
    apply Kf_unfold.
    ∃ ({|TR_zero _|} ∪ {|TR_one _|}).
    hinduction.
    - destruct x as [ [ ] | [ ] ].
      × apply (tr (inl (tr idpath))).
      × apply (tr (inr (tr idpath))).
    - intros.
      apply path_ishprop.
  Defined.

  Definition p (a : Unit + Unit) : X :=
    match a with
    | inl _ ⇒ TR_zero _
    | inr _ ⇒ TR_one _
    end.

  Instance p_surj : IsSurjection p.
  Proof.
    apply BuildIsSurjection.
    hinduction.
    - destruct x as [[ ] | [ ]].
      × apply tr. ∃ (inl tt). reflexivity.
      × apply tr. ∃ (inr tt). reflexivity.
    - intros.
      apply path_ishprop.
  Defined.

  Lemma LEM `{IsProjective X} : P + ¬P.
  Proof.
    pose (k := projective p idmap _).
    unfold hexists in k.
    simple refine (Trunc_rec _ k); clear k; intros [g Hg].
    destruct (dec (g (TR_zero _) = g (TR_one _))) as [Hℵ | Hℵ].
    - left.
      assert (TR_zero (BuildhProp P) = TR_one _) as Hbc.
      { pose (ap p Hℵ) as Hα.
        rewrite (ap (fun h ⇒ h (TR_zero _)) Hg) in Hα.
        rewrite (ap (fun h ⇒ h (TR_one _)) Hg) in Hα.
        assumption. }
      refine (classes_eq_related _ _ _ Hbc).
    - right. intros HP.
      apply Hℵ.
      refine (ap g (related_classes_eq _ _)).
      apply HP.
  Defined.
End k_fin_projective_lem.