Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Adjunctions.Core.

Local Open Scope cat.

Definition forms_equivalence {A B : category} (X : adjunction_data A B)
  (η := adjunit X) (ε := adjcounit X) : UU
  := (∏ a, is_iso (η a)) × (∏ b, is_iso (ε b)).

Definition equivalence_of_cats (A B : category) : UU
  := ∑ (X : adjunction_data A B), forms_equivalence X.

Coercion adjunction_data_from_equivalence_of_cats {A B}
         (X : equivalence_of_cats A B) : adjunction_data A B := pr1 X.

Definition adj_equivalence_of_cats {A B : category} (F : functor A B) : UU :=
   ∑ (H : is_left_adjoint F), forms_equivalence H.

Definition adj_from_equiv (D1 D2 : category) (F : functor D1 D2):
    adj_equivalence_of_cats F → is_left_adjoint F := λ x, pr1 x.
Coercion adj_from_equiv : adj_equivalence_of_cats >-> is_left_adjoint.

Definition make_adj_equivalence_of_cats {A B : category} (F : functor A B)
           (G : functor B A) η ε
           (H1 : form_adjunction F G η ε)
           (H2 : forms_equivalence ((F,,G,,η,,ε)))
  : adj_equivalence_of_cats F.
Proof.
  use tpair.
  - ∃ G. ∃ (η,,ε). apply H1.
  - apply H2.
Defined.

Definition adj_equivalence_inv {A B : category}
  {F : functor A B} (HF : adj_equivalence_of_cats F) : functor B A :=
    right_adjoint (pr1 HF).

Local Notation "HF ^^-1" := (adj_equivalence_inv HF)(at level 3).

Section Accessors.
  Context {A B : category} {F : functor A B} (HF : adj_equivalence_of_cats F).

  Definition unit_pointwise_iso_from_adj_equivalence :
      ∏ a, iso a (HF^^-1 (F a)).
  Proof.
  intro a.
  ∃ (unit_from_left_adjoint (pr1 HF) a).
  exact (pr1 (pr2 HF) a).
  Defined.

  Definition counit_pointwise_iso_from_adj_equivalence :
      ∏ b, iso (F (HF^^-1 b)) b.
  Proof.
    intro b.
    ∃ (counit_from_left_adjoint (pr1 HF) b).
    exact (pr2 (pr2 HF) b).
  Defined.

  Definition unit_nat_iso_from_adj_equivalence_of_cats :
    nat_iso (functor_identity A) (functor_composite F (right_adjoint (pr1 HF))).
  Proof.
    ∃ (unit_from_left_adjoint (pr1 HF)).
    exact (dirprod_pr1 (pr2 HF)).
  Defined.

  Definition counit_nat_iso_from_adj_equivalence_of_cats :
    nat_iso (functor_composite (right_adjoint (pr1 HF)) F) (functor_identity B).
  Proof.
    ∃ (counit_from_left_adjoint (pr1 HF)).
    exact (dirprod_pr2 (pr2 HF)).
  Defined.

  Definition unit_iso_from_adj_equivalence_of_cats :
    iso (C:=[A, A]) (functor_identity A)
        (functor_composite F (right_adjoint (pr1 HF))).
  Proof.
    ∃ (unit_from_left_adjoint (pr1 HF)).
    apply functor_iso_if_pointwise_iso. intro c.
    apply (pr1 (pr2 HF)).
  Defined.

  Definition counit_iso_from_adj_equivalence_of_cats :
    iso (C:=[B, B]) (functor_composite (right_adjoint (pr1 HF)) F)
        (functor_identity B).
  Proof.
    ∃ (counit_from_left_adjoint (pr1 HF)).
    apply functor_iso_if_pointwise_iso. intro c.
    apply (pr2 (pr2 HF)).
  Defined.
End Accessors.

Lemma triangle_2_from_1 {C D}
  (A : adjunction_data C D)
  (E : forms_equivalence A)
: triangle_1_statement A → triangle_2_statement A.
Proof.
  destruct A as [F [G [η ε]]].
  destruct E as [Hη Hε]; cbn in Hη, Hε.
  unfold triangle_1_statement, triangle_2_statement; cbn.
  intros T1 x.
  assert (etaH := nat_trans_ax η); cbn in etaH.
  assert (epsH := nat_trans_ax ε); cbn in epsH.


  apply (invmaponpathsweq (make_weq _ (iso_comp_left_isweq (make_iso _ (Hη _ )) _ ))).
  cbn.
  apply pathsinv0. etrans. apply id_left. etrans. apply (! id_right _ ).
  apply pathsinv0.
  apply (iso_inv_to_left _ _ _ (make_iso _ (Hη _ ))).
  apply (invmaponpathsweq (make_weq _ (iso_comp_left_isweq (functor_on_iso G (make_iso _ (Hε _ ))) _ ))).
  cbn.
  set (XR := functor_on_iso_is_iso _ _ G _ _ (make_iso _ (Hε x))).
  set (XR' := make_iso (#G (ε x)) XR). cbn in XR'.
  apply pathsinv0. etrans. apply id_left. etrans. apply (! id_right _ ).
  apply pathsinv0.
  apply (iso_inv_to_left _ _ _ XR').
  unfold XR', XR; clear XR' XR.

  repeat rewrite assoc.
  set (i := inv_from_iso
    (make_iso (# G (ε x))
       (functor_on_iso_is_iso D C G (F (G x)) x (make_iso (ε x) (Hε x))))).

  set (i' := inv_from_iso (make_iso (η (G x)) (Hη (G x)))).

  etrans. apply cancel_postcomposition. repeat rewrite <- assoc.
          rewrite etaH. apply idpath.
  etrans. repeat rewrite <- assoc. rewrite <- functor_comp.
          rewrite (epsH). rewrite functor_comp. apply idpath.
  etrans. apply maponpaths. apply maponpaths. repeat rewrite assoc. rewrite etaH.
          apply cancel_postcomposition. rewrite <- assoc. rewrite <- functor_comp.
          rewrite T1. rewrite functor_id. apply id_right.
  etrans. apply maponpaths. rewrite assoc. apply cancel_postcomposition.
          use (iso_after_iso_inv (make_iso _ (Hη _ ))).
  rewrite id_left.
  apply (iso_after_iso_inv ).
Defined.

Section adjointification.

Context {C D : category} (E : equivalence_of_cats C D).
Let F : functor C D := left_functor E.
Let G : functor D C := right_functor E.

Let ηntiso : iso (C:= [C,C]) (functor_identity _ ) (F ∙ G).
Proof.
  use functor_iso_from_pointwise_iso.
  use (adjunit E). intro c.
  apply (pr1 (pr2 E)).
Defined.

Let εntiso : iso (C:= [D,D]) (G ∙ F) (functor_identity _ ).
Proof.
  use functor_iso_from_pointwise_iso.
  use (adjcounit E). intro c.
  apply (pr2 (pr2 E)).
Defined.

Let FF : functor [D,D] [C, D]
  := (pre_comp_functor F).

Let GG : functor [C, D] [D, D]
  := (pre_comp_functor G).

Definition ε'ntiso : iso (C:= [D,D]) (G ∙ F) (functor_identity _ ).
Proof.
  eapply iso_comp.
    set (XR := functor_on_iso GG (functor_on_iso FF εntiso)).
    set (XR':= iso_inv_from_iso XR). apply XR'.
  eapply iso_comp.
     2: apply εntiso.
  set (XR := functor_on_iso (pre_comp_functor G) (iso_inv_from_iso ηntiso)).
  set (XR':= functor_on_iso (post_comp_functor F) XR).
  apply XR'.
Defined.

Definition adjointification_triangle_1
  : triangle_1_statement (F,,G,,pr1 ηntiso,,pr1 ε'ntiso).
Proof.
  intro x. cbn. rewrite id_right. rewrite id_right. rewrite id_right. rewrite id_right.
              repeat rewrite assoc.
  assert (ηinvH := nat_trans_ax (inv_from_iso ηntiso)).
  cbn in ηinvH. simpl in ηinvH.
  assert (εinvH := nat_trans_ax (inv_from_iso εntiso)).
  cbn in εinvH. simpl in εinvH.
  etrans. apply cancel_postcomposition. apply cancel_postcomposition.
          etrans. apply maponpaths. apply (! (id_right _ )).
          apply εinvH.
          rewrite id_right.
  repeat rewrite assoc. rewrite assoc4.
  apply id_conjugation.
  - etrans. eapply pathsinv0. apply functor_comp.
    etrans. apply maponpaths. etrans. apply maponpaths. eapply pathsinv0. apply id_right.
            apply ηinvH.
    etrans. apply maponpaths.
    apply (nat_trans_inv_pointwise_inv_before _ _ _ _ _ ηntiso (pr2 ηntiso)).
    apply functor_id.
  - assert (XR := nat_trans_inv_pointwise_inv_before _ _ _ _ _ εntiso (pr2 εntiso)).
    cbn in XR.
    etrans. apply cancel_postcomposition. eapply pathsinv0. apply id_right. apply XR.
Qed.

Lemma adjointification_forms_equivalence :
  forms_equivalence (F,, G,, pr1 ηntiso,, pr1 ε'ntiso).
Proof.
  split.
  - cbn. apply (is_functor_iso_pointwise_if_iso _ _ _ _ _ ηntiso (pr2 ηntiso)).
  - cbn. apply (is_functor_iso_pointwise_if_iso _ _ _ _ _ ε'ntiso (pr2 ε'ntiso)).
Qed.

Definition adjointification_triangle_2
  : triangle_2_statement (F,,G,,pr1 ηntiso,,pr1 ε'ntiso).
Proof.
  use triangle_2_from_1.
  - apply adjointification_forms_equivalence.
  - apply adjointification_triangle_1.
Qed.

Definition adjointificiation : adj_equivalence_of_cats F.
Proof.
  use make_adj_equivalence_of_cats.
  - exact G.
  - apply ηntiso.
  - apply ε'ntiso.
  - ∃ adjointification_triangle_1.
    apply adjointification_triangle_2.
  - apply adjointification_forms_equivalence.
Defined.

End adjointification.

Lemma identity_functor_is_adj_equivalence {A : category} :
  adj_equivalence_of_cats (functor_identity A).
Proof.
  use tpair.
  - exact is_left_adjoint_functor_identity.
  - now split; intros a; apply identity_is_iso.
Defined.

Lemma adj_equiv_of_cats_is_weq_of_objects (A B : category)
   (HA : is_univalent A) (HB : is_univalent B) (F : [A, B, B ])
   (HF : adj_equivalence_of_cats F) : isweq (pr1 (pr1 F)).
Proof.
  set (G := right_adjoint (pr1 HF)).
  set (et := unit_iso_from_adj_equivalence_of_cats HF).
  set (ep := counit_iso_from_adj_equivalence_of_cats HF).
  set (AAcat := is_univalent_functor_category A _ HA).
  set (BBcat := is_univalent_functor_category B _ HB).
  set (Et := isotoid _ AAcat et).
  set (Ep := isotoid _ BBcat ep).
  apply (isweq_iso _ (λ b, pr1 (right_adjoint (pr1 HF)) b)); intro a.
  apply (!toforallpaths _ _ _ (base_paths _ _ (base_paths _ _ Et)) a).
  now apply (toforallpaths _ _ _ (base_paths _ _ (base_paths _ _ Ep))).
Defined.

Definition weq_on_objects_from_adj_equiv_of_cats (A B : category)
   (HA : is_univalent A) (HB : is_univalent B) (F : ob [A, B, B])
   (HF : adj_equivalence_of_cats F) : weq
          (ob A) (ob B).
Proof.
  ∃ (pr1 (pr1 F)).
  now apply (@adj_equiv_of_cats_is_weq_of_objects _ _ HA).
Defined.

Lemma isaprop_sigma_iso (A B : category) (HA : is_univalent A)
     (F : functor A B) (HF : fully_faithful F) :
     ∏ b : ob B, isaprop (∑ a : ob A, iso (F a) b).
Proof.
  intro b.
  apply invproofirrelevance.
  intros x x'; destruct x as [a f]; destruct x' as [a' f'].
  set (fminusf := iso_comp f (iso_inv_from_iso f')).
  set (g := iso_from_fully_faithful_reflection HF fminusf).
  apply (two_arg_paths_f (B:=λ a', iso ((pr1 F) a') b) (isotoid _ HA g)).
  intermediate_path (iso_comp (iso_inv_from_iso
    (functor_on_iso F (idtoiso (isotoid _ HA g)))) f).
  - generalize (isotoid _ HA g).
    intro p0; destruct p0.
    rewrite <- functor_on_iso_inv. simpl.
    rewrite iso_inv_of_iso_id.
    apply eq_iso.
    simpl; rewrite functor_id.
    rewrite id_left.
    apply idpath.
  - rewrite idtoiso_isotoid.
    unfold g; clear g.
    unfold fminusf; clear fminusf.
    assert (HFg : functor_on_iso F
          (iso_from_fully_faithful_reflection HF
            (iso_comp f (iso_inv_from_iso f'))) =
            iso_comp f (iso_inv_from_iso f')).
    + generalize (iso_comp f (iso_inv_from_iso f')).
      intro h.
      apply eq_iso; simpl.
      set (H3:= homotweqinvweq (weq_from_fully_faithful HF a a')).
      simpl in H3. unfold fully_faithful_inv_hom.
      unfold invweq; simpl.
      rewrite H3; apply idpath.
    + rewrite HFg.
      rewrite iso_inv_of_iso_comp.
      apply eq_iso; simpl.
      repeat rewrite <- assoc.
      rewrite iso_after_iso_inv.
      rewrite id_right.
      set (H := iso_inv_iso_inv _ _ f').
      now apply (base_paths _ _ H).
Qed.

Lemma isaprop_split_essentially_surjective (A B : category) (HA : is_univalent A)
      (F : functor A B) (HF : fully_faithful F) :
  isaprop (split_essentially_surjective F).
Proof.
  apply impred; intro.
  now apply isaprop_sigma_iso.
Qed.

Lemma ff_essentially_surjective_to_split (A B : category) (HA : is_univalent A)
      (F : functor A B) (HF : fully_faithful F) (HF' : essentially_surjective F) :
  split_essentially_surjective F.
Proof.
  intro b.
  apply (squash_to_prop (HF' b)).
  - apply isaprop_sigma_iso; assumption.
  - exact (idfun _).
Defined.

Section from_fully_faithful_and_ess_surj_to_equivalence.

Variables A B : category.
Hypothesis HA : is_univalent A.
Variable F : functor A B.
Hypothesis HF : fully_faithful F.
Hypothesis HS : essentially_surjective F.

Definition rad_ob : ob B → ob A.
Proof.
  use split_essentially_surjective_inv_on_obj.
  - exact F.
  - apply ff_essentially_surjective_to_split; assumption.
Defined.

Definition rad_eps (b : ob B) : iso (pr1 F (rad_ob b)) b.
Proof.
  apply (pr2 (HS b (tpair (λ x, isaprop x) _
               (isaprop_sigma_iso A B HA F HF b)) (λ x, x))).
Defined.

Definition rad_mor (b b' : ob B) (g : b --> b') : rad_ob b --> rad_ob b'.
Proof.
  set (epsgebs' := rad_eps b · g · iso_inv_from_iso (rad_eps b')).
  set (Gg := fully_faithful_inv_hom HF (rad_ob b) _ epsgebs').
  exact Gg.
Defined.

Definition rad_eta (a : ob A) : a --> rad_ob (pr1 F a).
Proof.
  set (epsFa := inv_from_iso (rad_eps (pr1 F a))).
  exact (fully_faithful_inv_hom HF _ _ epsFa).
Defined.

Definition rad_functor_data : functor_data B A.
Proof.
  ∃ rad_ob.
  exact rad_mor.
Defined.

Lemma rad_is_functor : is_functor rad_functor_data.
Proof.
  split. simpl.
  intro b. simpl . unfold rad_mor . simpl .
  rewrite id_right,
  iso_inv_after_iso,
  fully_faithful_inv_identity.
  apply idpath.

  intros a b c f g. simpl .
  unfold rad_mor; simpl.
  rewrite <- fully_faithful_inv_comp.
  apply maponpaths.
  repeat rewrite <- assoc.
  repeat apply maponpaths.
  rewrite assoc.
  rewrite iso_after_iso_inv, id_left.
  apply idpath.
Qed.

Definition rad : ob [B, A, A].
Proof.
  ∃ rad_functor_data.
  apply rad_is_functor.
Defined.

Lemma rad_eps_is_nat_trans : is_nat_trans
    (functor_composite rad F) (functor_identity B)
       (λ b, rad_eps b).
Proof.
  unfold is_nat_trans.
  simpl.
  intros b b' g.
  unfold rad_mor; unfold fully_faithful_inv_hom.
  set (H3 := homotweqinvweq (weq_from_fully_faithful HF (pr1 rad b) (pr1 rad b'))).
  simpl in ×.
  rewrite H3; clear H3.
  repeat rewrite <- assoc.
  rewrite iso_after_iso_inv, id_right.
  apply idpath.
Qed.

Definition rad_eps_trans : nat_trans _ _ :=
   tpair (is_nat_trans _ _ ) _ rad_eps_is_nat_trans.

Ltac inv_functor x y :=
   let H:=fresh in
   set (H:= homotweqinvweq (weq_from_fully_faithful HF x y));
     simpl in H;
     unfold fully_faithful_inv_hom; simpl;
     rewrite H; clear H.

Lemma rad_eta_is_nat_trans : is_nat_trans
         (functor_identity A) (functor_composite F rad)
       (λ a, rad_eta a).
Proof.
  unfold is_nat_trans.
  simpl.
  intros a a' f.
  unfold rad_mor. simpl.
  apply (invmaponpathsweq
          (weq_from_fully_faithful HF a (rad_ob ((pr1 F) a')))).
  simpl; repeat rewrite functor_comp.
  unfold rad_eta.
  set (HHH := rad_eps_is_nat_trans (pr1 F a) (pr1 F a')).
  simpl in HHH; rewrite <- HHH; clear HHH.
  inv_functor a' (rad_ob ((pr1 F) a')).
  inv_functor a (rad_ob ((pr1 F) a)).
  inv_functor (rad_ob (pr1 F a)) (rad_ob ((pr1 F) a')).
  unfold rad_mor. simpl.
  repeat rewrite <- assoc.
  rewrite iso_inv_after_iso.
  rewrite id_right.
  inv_functor (rad_ob (pr1 F a)) (rad_ob ((pr1 F) a')).
  repeat rewrite assoc.
  rewrite iso_after_iso_inv.
  rewrite id_left.
  apply idpath.
Qed.

Definition rad_eta_trans : nat_trans _ _ :=
   tpair (is_nat_trans _ _ ) _ rad_eta_is_nat_trans.

Lemma rad_form_adjunction : form_adjunction F rad rad_eta_trans rad_eps_trans.
Proof.
  split; simpl.
  - intro a. cbn.
    unfold rad_eta.
    inv_functor a (rad_ob (pr1 F a)).
    apply iso_after_iso_inv.
  - intro b.
    apply (invmaponpathsweq
             (weq_from_fully_faithful HF (rad_ob b) (rad_ob b))).
    simpl; rewrite functor_comp.
    unfold rad_eta.
    inv_functor (rad_ob b) (rad_ob (pr1 F (rad_ob b))).
    unfold rad_mor.
    inv_functor (rad_ob (pr1 F (rad_ob b))) (rad_ob b).
    repeat rewrite assoc.
    rewrite iso_after_iso_inv.
    rewrite <- assoc.
    rewrite iso_inv_after_iso.
    rewrite id_left.
    rewrite functor_id.
    apply idpath.
Qed.

Definition rad_are_adjoints : are_adjoints F rad.
Proof.
  ∃ (make_dirprod rad_eta_trans rad_eps_trans).
  apply rad_form_adjunction.
Defined.

Definition rad_is_left_adjoint : is_left_adjoint F.
Proof.
  ∃ rad.
  apply rad_are_adjoints.
Defined.

Lemma rad_equivalence_of_cats : adj_equivalence_of_cats F.
Proof.
  ∃ rad_is_left_adjoint.
  split; simpl.
  intro a.
  unfold rad_eta.
  set (H := fully_faithful_reflects_iso_proof _ _ _ HF
       a (rad_ob ((pr1 F) a))).
  simpl in ×.
  set (H' := H (iso_inv_from_iso (rad_eps ((pr1 F) a)))).
  change ((fully_faithful_inv_hom HF a (rad_ob ((pr1 F) a))
     (inv_from_iso (rad_eps ((pr1 F) a))))) with
      (fully_faithful_inv_hom HF a (rad_ob ((pr1 F) a))
     (iso_inv_from_iso (rad_eps ((pr1 F) a)))).
  apply H'.
  intro b. apply (pr2 (rad_eps b)).
Defined.

End from_fully_faithful_and_ess_surj_to_equivalence.