(* Bishop-finiteness is that "default" notion of finiteness in the HoTT library *)
Require Import HoTT HitTactics.
Require Import Sub notation variations.k_finite.
Require Import fsets.properties.

Section finite_hott.
  Variable (A : Type).
  Context `{Univalence} `{IsHSet A}.

  (* A subobject is B-finite if its extension is B-finite as a type *)
  Definition Bfin (X : Sub A) : hProp := BuildhProp (Finite {a : A & a ∈ X}).

  Global Instance singleton_contr a : Contr {b : A & b ∈ {|a|}}.
  Proof.
    exists (a; tr idpath).
    intros [b p].
    simple refine (Trunc_ind (fun p => (a; tr 1%path) = (b; p)) _ p).
    clear p; intro p. simpl.
    apply path_sigma' with (p^).
    apply path_ishprop.
  Defined.
  
  Definition singleton_fin_equiv' a : Fin 1 -> {b : A & b ∈ {|a|}}.
  Proof.  
    intros _. apply (center {b : A & b ∈ {|a|}}).
  Defined.

  Global Instance singleton_fin_equiv a : IsEquiv (singleton_fin_equiv' a).
  Proof. apply _. Defined.

  Definition singleton : closedSingleton Bfin.
  Proof.
    intros a.
    simple refine (Build_Finite _ 1 _).
    apply tr.
    symmetry.
    refine (BuildEquiv _ _ (singleton_fin_equiv' a) _).
  Defined.

  Definition empty_finite : closedEmpty Bfin.
  Proof.
    simple refine (Build_Finite _ 0 _).
    apply tr.
    simple refine (BuildEquiv _ _ _ _).
    intros [a p]; apply p.
  Defined.

  Definition decidable_empty_finite : hasDecidableEmpty Bfin.
  Proof.
    intros X Y.
    destruct Y as [n Xn].
    strip_truncations.
    destruct Xn as [f [g fg gf adj]].
    destruct n.
    - refine (tr(inl _)).
      apply path_forall. intro z.
      apply path_iff_hprop.
      * intros p.
        contradiction (f (z;p)).
      * contradiction.
    - refine (tr(inr _)).
      apply (tr(g(inr tt))).
  Defined.
  
  Lemma no_union
        (f : forall (X Y : Sub A),
            Bfin X -> Bfin Y -> Bfin (X ∪ Y))
        (a b : A) :
      hor (a = b) (a = b -> Empty).
  Proof.
    specialize (f {|a|} {|b|} (singleton a) (singleton b)).
    unfold Bfin in f.
    destruct f as [n pn].
    strip_truncations.
    destruct pn as [f [g fg gf _]].
    destruct n as [|n].
    unfold Sect in *.
    - contradiction f.
      exists a. apply (tr(inl(tr idpath))).
    - destruct n as [|n].
      + (* If the size of the union is 1, then (a = b) *)
        refine (tr (inl _)).
        pose (s1 := (a;tr(inl(tr idpath)))
               : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
        pose (s2 := (b;tr(inr(tr idpath)))
               : {c : A & Trunc (-1) (Trunc (-1) (c = a) + Trunc (-1) (c = b))}).
        refine (ap (fun x => x.1) (gf s1)^ @ _ @ (ap (fun x => x.1) (gf s2))).
        assert (fs_eq : f s1 = f s2).
        { by apply path_ishprop. }
        refine (ap (fun x => (g x).1) fs_eq).
      + (* Otherwise, ¬(a = b) *)
        refine (tr (inr _)).
        intros p.
        pose (s1 := inl (inr tt) : Fin n + Unit + Unit).
        pose (s2 := inr tt : Fin n + Unit + Unit).
        pose (gs1 := g s1).
        pose (c := g s1).
        pose (gs2 := g s2).
        pose (d := g s2).
        assert (Hgs1 : gs1 = c) by reflexivity.
        assert (Hgs2 : gs2 = d) by reflexivity.
        destruct c as [x px'].
        destruct d as [y py'].        
        simple refine (Trunc_ind _ _ px') ; intros px.
        simple refine (Trunc_ind _ _ py') ; intros py.
        simpl.
        cut (x = y).
        {
          enough (s1 = s2) as X.
          {
            intros. 
            unfold s1, s2 in X.
            refine (not_is_inl_and_inr' (inl(inr tt)) _ _).
            + apply tt.
            + rewrite X ; apply tt.
          }
          transitivity (f gs1).
          { apply (fg s1)^. }
          symmetry ; transitivity (f gs2).
          { apply (fg s2)^. }
          rewrite Hgs1, Hgs2.
          f_ap.
          simple refine (path_sigma _ _ _ _ _); [ | apply path_ishprop ]; simpl.
          destruct px as [p1 | p1] ; destruct py as [p2 | p2] ; strip_truncations.
          * apply (p2 @ p1^).
          * refine (p2 @ _^ @ p1^). auto.
          * refine (p2 @ _ @ p1^). auto.
          * apply (p2 @ p1^).
        }
        destruct px as [px | px] ; destruct py as [py | py]; strip_truncations.
        ** apply (px @ py^).
        ** refine (px @ _ @ py^). auto.
        ** refine (px @ _ @ py^). symmetry. auto.
        ** apply (px @ py^).
  Defined.

  Section empty.
    Variable (X : A -> hProp)
             (Xequiv : {a : A & a ∈ X} <~> Fin 0).

    Lemma X_empty : X = ∅.
    Proof.
      apply path_forall.
      intro z.
      apply path_iff_hprop ; try contradiction.
      intro x.
      destruct Xequiv as [f fequiv].
      contradiction (f(z;x)).
    Defined.
    
  End empty.
  
  Section split.
    Variable (X : A -> hProp)
             (n : nat)
             (Xequiv : {a : A & a ∈ X} <~> Fin n + Unit).

    Definition split : {X' : A -> hProp & {a : A & a ∈ X'} <~> Fin n}.
    Proof.
      destruct Xequiv as [f [g fg gf adj]].
      unfold Sect in *. 
      pose (fun x : A => sig (fun y : Fin n => x = (g(inl y)).1 )) as X'.
      assert (forall a : A, IsHProp (X' a)).
      {
        intros.
        unfold X'.
        apply hprop_allpath.
        intros [x px] [y py].
        simple refine (path_sigma _ _ _ _ _).
        * cbn.
          pose (f(g(inl x))) as fgx.
          cut (g(inl x) = g(inl y)).
          {
            intros q.
            pose (ap f q).
            rewrite !fg in p.
            refine (path_sum_inl _ p).
          }
          apply path_sigma with (px^ @ py).
          apply path_ishprop.
        * apply path_ishprop.          
      }
      pose (fun a => BuildhProp(X' a)) as Y.
      exists Y.
      unfold Y, X'.
      cbn.
      unshelve esplit.
      - intros [a [y p]]. apply y.
      - apply isequiv_biinv.
        unshelve esplit.
        * exists (fun x => (( (g(inl x)).1 ;(x;idpath)))).
          unfold Sect.
          intros [a [y p]].
          apply path_sigma with p^.
          simpl.
          rewrite transport_sigma.
          simple refine (path_sigma _ _ _ _ _) ; simpl.
          ** rewrite transport_const ; reflexivity.
          ** apply path_ishprop.
        * exists (fun x => (( (g(inl x)).1 ;(x;idpath)))).
          unfold Sect.
          intros x.
          reflexivity.
    Defined.
    
    Definition new_el : {a' : A & forall z, X z =
                                            lor (split.1 z) (merely (z = a'))}.
    Proof.
      exists ((Xequiv^-1 (inr tt)).1).
      intros.
      apply path_iff_hprop.
      - intros Xz.
        pose (Xequiv (z;Xz)) as fz.
        pose (c := fz).
        assert (c = fz). reflexivity.
        destruct c as [fz1 | fz2].
        * refine (tr(inl _)).
          unfold split ; simpl.
          exists fz1.
          rewrite X0.
          unfold fz.
          destruct Xequiv as [? [? ? sect ?]].
          compute.
          rewrite sect.
          reflexivity.
        * refine (tr(inr(tr _))).
          destruct fz2.
          rewrite X0.
          unfold fz.
          rewrite eissect.
          reflexivity.
      - intros X0.
        strip_truncations.
        destruct X0 as [Xl | Xr].
        * unfold split in Xl ; simpl in Xl.
          destruct Xequiv as [f [g fg gf adj]].
          destruct Xl as [m p].
          rewrite p.
          apply (g (inl m)).2.
        * strip_truncations.
          rewrite Xr.
          apply ((Xequiv^-1(inr tt)).2).
    Defined.

  End split.
End finite_hott.

Arguments Bfin {_} _.

Section dec_membership.
  Variable (A : Type).
  Context `{DecidablePaths A} `{Univalence}.
  Global Instance DecidableMembership (P : Sub A) (Hfin : Bfin P) (a : A) :
    Decidable (a ∈ P).
  Proof.
    destruct Hfin as [n Hequiv].
    strip_truncations.
    revert Hequiv.
    revert P.
    induction n.
    - intros.
      pose (X_empty _ P Hequiv) as p.
      rewrite p.
      apply _.
    - intros.
      pose (new_el _ P n Hequiv) as b.
      destruct b as [b HX'].
      destruct (split _ P n Hequiv) as [X' X'equiv]. simpl in HX'.
      unfold member, sub_membership.
      rewrite (HX' a).
      pose (IHn X' X'equiv) as IH.
      destruct IH as [IH | IH].
      + left. apply (tr (inl IH)).
      + destruct (dec (a = b)) as [Hab | Hab].
        left. apply (tr (inr (tr Hab))).
        right. intros α. strip_truncations.
        destruct α as [β | γ]; [ | strip_truncations]; contradiction.
  Defined.
End dec_membership.

Section cowd.
  Variable (A : Type).
  Context `{DecidablePaths A} `{Univalence}.

  Definition cow := { X : Sub A | Bfin X}.
  Definition empty_cow : cow.
  Proof.
    exists empty. apply empty_finite.
  Defined.

  Definition add_cow : forall a : A, cow -> cow.
  Proof.
    intros a [X PX].
    exists (fun z => lor (X z) (merely (z = a))).
    destruct (dec (a ∈ X)) as [Ha | Ha];
      destruct PX as [n PX];
      strip_truncations.
    - (* a ∈ X *)
      exists n. apply tr.
      transitivity ({a : A & a ∈ X}); [ | apply PX ].
      apply equiv_functor_sigma_id.
      intro a'. eapply equiv_iff_hprop_uncurried ; split; cbn.
      + intros Ha'. strip_truncations.
        destruct Ha' as [HXa' | Haa'].
        * assumption.
        * strip_truncations. rewrite Haa'. assumption.
      + intros HXa'. apply tr.
        left. assumption.
    - (* a ∉ X *)
      exists (S n). apply tr.
      destruct PX as [f [g Hfg Hgf adj]].
      unshelve esplit.
      + intros [a' Ha']. cbn in Ha'.
        destruct (dec (a' = a)) as [Haa' | Haa'].
        * right. apply tt.
        * assert (X a') as HXa'.
          { strip_truncations.
            destruct Ha' as [Ha' | Ha']; [ assumption | ].
            strip_truncations. by (contradiction (Haa' Ha')). }
          apply (inl (f (a';HXa'))).
      + apply isequiv_biinv; simpl.
        unshelve esplit; simpl.
        * unfold Sect; simpl.
          simple refine (_;_).
          { destruct 1 as [M | ?].
            - destruct (g M) as [a' Ha'].
              exists a'. apply tr.
                by left.
            - exists a. apply (tr (inr (tr idpath))). }
          simpl. intros [a' Ha'].
          strip_truncations.
          destruct Ha' as [HXa' | Haa']; simpl;
            destruct (dec (a' = a)); simpl.
          ** apply path_sigma' with p^. apply path_ishprop.
          ** rewrite Hgf; cbn. done.
          ** apply path_sigma' with p^. apply path_ishprop.
          ** rewrite Hgf; cbn. apply path_sigma' with idpath. apply path_ishprop.
        * unfold Sect; simpl.
          simple refine (_;_).
          { destruct 1 as [M | ?].
            - destruct (g M) as [a' Ha'].
              exists a'. apply tr.
                by left.
            - exists a. apply (tr (inr (tr idpath))). }
          simpl. intros [M | [] ].
          ** destruct (dec (_ = a)) as [Haa' | Haa']; simpl.
             { destruct (g M) as [a' Ha']. rewrite Haa' in Ha'. by contradiction. }
             { f_ap. }
          ** destruct (dec (a = a)); try by contradiction.
             reflexivity.
  Defined.

  Theorem cowy
    (P : cow -> hProp)
    (doge : P empty_cow)
    (koeientaart : forall a c, P c -> P (add_cow a c))
    :
    forall X : cow, P X.
  Proof.
    intros [X [n FX]]. strip_truncations.
    revert X FX.
    induction n; intros X FX.
    - pose (HX_emp:= X_empty _ X FX).
      assert ((X; Build_Finite _ 0 (tr FX)) = empty_cow) as HX.
      { apply path_sigma' with HX_emp. apply path_ishprop. }
      rewrite HX. assumption.
    - pose (a' := new_el _ X n FX).
      destruct a' as [a' Ha'].
      destruct (split _ X n FX) as [X' FX'].
      pose (X'cow := (X'; Build_Finite _ n (tr FX')) : cow).
      assert ((X; Build_Finite _ (n.+1) (tr FX)) = add_cow a' X'cow) as ℵ.
      { simple refine (path_sigma' _ _ _); [ | apply path_ishprop ].
        apply path_forall. intros a.
        unfold X'cow.
        specialize (Ha' a). rewrite Ha'. simpl. reflexivity. }
      rewrite ℵ.
      apply koeientaart.
      apply IHn.
  Defined.

  Definition bfin_to_kfin : forall (X : Sub A), Bfin X -> Kf_sub _ X.
  Proof.
    intros X BFinX.
    unfold Bfin in BFinX.
    destruct BFinX as [n iso].
    strip_truncations.
    revert iso ; revert X.
    induction n ; unfold Kf_sub, Kf_sub_intern.
    - intros.
      exists ∅.
      apply path_forall.
      intro z.
      simpl in *.
      apply path_iff_hprop ; try contradiction.
      destruct iso as [f f_equiv].
      apply (fun Xz => f(z;Xz)).
    - intros.
      simpl in *.
      destruct (new_el _ X n iso) as [a HXX'].
      destruct (split _ X n iso) as [X' X'equiv].
      destruct (IHn X' X'equiv) as [Y HY].
      exists (Y ∪ {|a|}).
      unfold map in *.
      apply path_forall.
      intro z.
      rewrite union_isIn.
      rewrite <- (ap (fun h => h z) HY).
      rewrite HXX'.
      cbn.
      reflexivity.
  Defined.

  Lemma kfin_is_bfin : @closedUnion A Bfin.
  Proof.
    intros X Y HX HY.
    pose (Xcow := (X; HX) : cow).
    pose (Ycow := (Y; HY) : cow).
    simple refine (cowy (fun C => Bfin (C.1 ∪ Y)) _ _ Xcow); simpl.
    - assert ((fun a => Trunc (-1) (Empty + Y a)) = (fun a => Y a)) as Help.
      { apply path_forall. intros z; simpl.
        apply path_iff_ishprop.
        + intros; strip_truncations; auto.
          destruct X0; auto. destruct e.
        + intros ?.  apply tr. right; assumption.
          (* TODO FIX THIS with sum_empty_l *)
      }
      rewrite Help. apply HY.
    - intros a [X' HX'] [n FX'Y]. strip_truncations.
      destruct (dec(a ∈ X')) as [HaX' | HaX'].
      * exists n. apply tr.
        transitivity ({a : A & Trunc (-1) (X' a + Y a)}); [| assumption ].
        apply equiv_functor_sigma_id. intro a'.
        apply equiv_iff_hprop.
        { intros Q. strip_truncations.
          destruct Q as [Q | Q].
          - strip_truncations.
            apply tr. left.
            destruct Q ; auto.
            strip_truncations. rewrite t; assumption.
          - apply (tr (inr Q)). }
        { intros Q. strip_truncations.
          destruct Q as [Q | Q]; apply tr.
          - left. apply tr. left. done.
          - right. done. }
      * destruct (dec (a ∈ Y)) as [HaY | HaY ].
        ** exists n. apply tr.
           transitivity ({a : A & Trunc (-1) (X' a + Y a)}); [| assumption ].
           apply equiv_functor_sigma_id. intro a'.
           apply equiv_iff_hprop.
           { intros Q. strip_truncations.
             destruct Q as [Q | Q].
             - strip_truncations.
               apply tr.
               destruct Q.
               left. auto.
               right. strip_truncations. rewrite t; assumption.
             - apply (tr (inr Q)). }
           { intros Q. strip_truncations.
             destruct Q as [Q | Q]; apply tr.
             - left. apply tr. left. done.
             - right. done. }
        ** exists (n.+1). apply tr.
           destruct FX'Y as [f [g Hfg Hgf adj]].
           unshelve esplit.
           { intros [a' Ha']. cbn in Ha'.
             destruct (dec (BuildhProp (a' = a))) as [Ha'a | Ha'a].
             - right. apply tt.
             - left. refine (f (a';_)).
               strip_truncations.
               destruct Ha' as [Ha' | Ha'].
               + strip_truncations.
                 destruct Ha' as [Ha' | Ha'].
                 * apply (tr (inl Ha')).
                 * strip_truncations. contradiction.
               + apply (tr (inr Ha')). }
           { apply isequiv_biinv; simpl.
             unshelve esplit; simpl.
             - unfold Sect; simpl.
               simple refine (_;_).
               { destruct 1 as [M | ?].
                 - destruct (g M) as [a' Ha'].
                   exists a'.
                   strip_truncations; apply tr.
                   destruct Ha' as [Ha' | Ha'].
                   + left. apply (tr (inl Ha')).
                   + right. done.
                 - exists a. apply (tr (inl (tr (inr (tr idpath))))). }
               { intros [a' Ha']; simpl.
                 strip_truncations.
                 destruct Ha' as [HXa' | Haa']; simpl;
                   destruct (dec (a' = a)); simpl.
                 ** apply path_sigma' with p^. apply path_ishprop.
                 ** rewrite Hgf; cbn. apply path_sigma' with idpath. apply path_ishprop.
                 ** apply path_sigma' with p^. apply path_ishprop.
                 ** rewrite Hgf; cbn. done. }
             - unfold Sect; simpl.
               simple refine (_;_).
               { destruct 1 as [M | ?].
                 - (* destruct (g M) as [a' Ha']. *)
                   exists (g M).1.
                   simple refine (Trunc_rec _ (g M).2).
                   intros Ha'.
                   apply tr.
                   (* strip_truncations; apply tr. *)
                   destruct Ha' as [Ha' | Ha'].
                   + left. apply (tr (inl Ha')).
                   + right. done.
                 - exists a. apply (tr (inl (tr (inr (tr idpath))))). }
               simpl. intros [M | [] ].
               ** destruct (dec (_ = a)) as [Haa' | Haa']; simpl.
                  { destruct (g M) as [a' Ha']. simpl in Haa'.
                    strip_truncations.
                    rewrite Haa' in Ha'. destruct Ha'; by contradiction. }
                  { f_ap. transitivity (f (g M)); [ | apply Hfg].
                    f_ap. apply path_sigma' with idpath.
                    apply path_ishprop. }
               ** destruct (dec (a = a)); try by contradiction.
                  reflexivity. }
  Defined.

End cowd.

Section Kf_to_Bf.
  Context `{Univalence}.

  Definition FSet_to_Bfin (A : Type) `{DecidablePaths A} : forall (X : FSet A), Bfin (map X).
  Proof.
    hinduction; try (intros; apply path_ishprop).
    - exists 0. apply tr. simpl.
      simple refine (BuildEquiv _ _ _ _).
      destruct 1 as [? []].
    - intros a.
      exists 1. apply tr. simpl.
      transitivity Unit; [ | symmetry; apply sum_empty_l ].
      unshelve esplit.
      + exact (fun _ => tt).
      + apply isequiv_biinv. split.
        * exists (fun _ => (a; tr(idpath))).
          intros [b Hb]. strip_truncations.
          apply path_sigma' with Hb^.
          apply path_ishprop.
        * exists (fun _ => (a; tr(idpath))).
          intros []. reflexivity.
    - intros Y1 Y2 HY1 HY2.
      apply kfin_is_bfin; auto.
  Defined.

  Instance Kf_to_Bf (X : Type) (Hfin : Kf X) `{DecidablePaths X} : Finite X.
  Proof.
    apply Kf_unfold in Hfin.
    destruct Hfin as [Y HY].
    pose (X' := FSet_to_Bfin _ Y).
    unfold Bfin in X'.
    simple refine (finite_equiv' _ _ X').
    unshelve esplit.
    - intros [a ?]. apply a.
    - apply isequiv_biinv. split.
      * exists (fun a => (a;HY a)).
        intros [b Hb].
        apply path_sigma' with idpath.
        apply path_ishprop.
      * exists (fun a => (a;HY a)).
        intros b. reflexivity.
  Defined.

End Kf_to_Bf.