Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.catiso.
Require Import UniMath.CategoryTheory.CategoryEquality.
Require Import UniMath.CategoryTheory.Adjunctions.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Bicat. Import Bicat.Notations.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Adjunctions.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.EquivToAdjequiv.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.AdjointUnique.
Require Import UniMath.CategoryTheory.Bicategories.Bicategories.Univalence.

Local Open Scope cat.

Definition cat_prebicat_data
  : prebicat_data.
Proof.
  use build_prebicat_data.
  - exact univalent_category.
  - exact (λ C D, functor C D).
  - exact (λ _ _ F G, nat_trans F G).
  - exact (λ C, functor_identity C).
  - exact (λ _ _ _ F G, functor_composite F G).
  - exact (λ _ _ F, nat_trans_id F).
  - exact (λ _ _ _ _ _ α β, nat_trans_comp _ _ _ α β).
  - exact (λ _ _ _ F _ _ α, pre_whisker F α).
  - exact (λ _ _ _ _ _ H α, post_whisker α H).
  - exact (λ _ _ F, nat_trans_id F).
  - exact (λ _ _ F, nat_trans_id F).
  - exact (λ _ _ F, nat_trans_id F).
  - exact (λ _ _ F, nat_trans_id F).
  - exact (λ _ _ _ _ _ _ _, nat_trans_id _).
  - exact (λ _ _ _ _ _ _ _, nat_trans_id _).
Defined.

Definition cat_prebicat_laws : prebicat_laws cat_prebicat_data.
Proof.
  repeat split; cbn.
  - intros C D F G η.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_left.
  - intros C D F G η.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_right.
  - intros C D F₁ F₂ F₃ F₄ α β γ.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply assoc.
  - intros C₁ C₂ C₃ F G.
    apply nat_trans_eq; try apply C₃.
    reflexivity.
  - intros C₁ C₂ C₃ F G.
    apply nat_trans_eq; try apply C₃.
    intros ; cbn.
    apply functor_id.
  - intros C₁ C₂ C₃ F G₁ G₂ G₃ α β.
    apply nat_trans_eq; try apply C₃.
    reflexivity.
  - intros C₁ C₂ C₃ F₁ F₂ F₃ G α β.
    apply nat_trans_eq; try apply C₃.
    intros ; cbn.
    exact (!(functor_comp G _ _)).
  - intros C D F G α.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    rewrite id_left, id_right.
    reflexivity.
  - intros C D F G α.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    rewrite id_left, id_right.
    reflexivity.
  - intros C₁ C₂ C₃ C₄ F G H₁ H₂ α.
    apply nat_trans_eq; try apply C₄.
    intros ; cbn.
    rewrite id_left, id_right.
    reflexivity.
  - intros C₁ C₂ C₃ C₄ F G₁ G₂ H α.
    apply nat_trans_eq; try apply C₄.
    intros ; cbn.
    rewrite id_left, id_right.
    reflexivity.
  - intros C₁ C₂ C₃ C₄ F₁ F₂ G H α.
    apply nat_trans_eq; try apply C₄.
    intros ; cbn.
    rewrite id_left, id_right.
    reflexivity.
  - intros C₁ C₂ C₃ F₁ F₂ G₁ H₂ α β.
    apply nat_trans_eq; try apply C₃.
    intros ; cbn.
    exact ((nat_trans_ax β _ _ _)).
  - intros C D F.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_left.
  - intros C D F.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_left.
  - intros C D F.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_left.
  - intros C D F.
    apply nat_trans_eq; try apply D.
    intros ; cbn.
    apply id_left.
  - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃.
    apply nat_trans_eq; try apply C₄.
    intros ; cbn.
    apply id_left.
  - intros C₁ C₂ C₃ C₄ F₁ F₂ F₃.
    apply nat_trans_eq; try apply C₄.
    intros ; cbn.
    apply id_left.
  - intros C₁ C₂ C₃ F G.
    apply nat_trans_eq; try apply C₃.
    intros ; cbn.
    exact (id_left _ @ functor_id G _).
  - intros C₁ C₂ C₃ C₄ C₅ F₁ F₂ F₃ F₄.
    apply nat_trans_eq; try apply C₅.
    intros ; cbn.
    rewrite !id_left.
    exact (functor_id F₄ _).
Qed.

Definition prebicat_of_cats : prebicat := _ ,, cat_prebicat_laws.

Lemma isaset_cells_prebicat_of_cats : isaset_cells prebicat_of_cats.
Proof.
  intros a b f g.
  apply isaset_nat_trans.
  apply homset_property.
Qed.

Definition bicat_of_cats : bicat
  := (prebicat_of_cats,, isaset_cells_prebicat_of_cats).

Definition is_invertible_2cell_to_is_nat_iso
           {C D : bicat_of_cats}
           {F G : C --> D}
           (η : F ==> G)
  : is_invertible_2cell η → is_nat_iso η.
Proof.
  intros Hη X.
  use is_iso_qinv.
  - apply (Hη^-1).
  - split ; cbn.
    + exact (nat_trans_eq_pointwise (vcomp_rinv Hη) X).
    + exact (nat_trans_eq_pointwise (vcomp_lid Hη) X).
Defined.

Definition invertible_2cell_to_nat_iso
           {C D : bicat_of_cats}
           (F G : C --> D)
  : invertible_2cell F G → nat_iso F G.
Proof.
  intros η.
  use mk_nat_iso.
  - exact (cell_from_invertible_2cell η).
  - apply is_invertible_2cell_to_is_nat_iso.
    apply η.
Defined.

Definition is_nat_iso_to_is_invertible_2cell
           {C D : bicat_of_cats}
           {F G : C --> D}
           (η : F ==> G)
  : is_nat_iso η → is_invertible_2cell η.
Proof.
  intros Hη.
  use tpair.
  - apply (nat_iso_inv (η ,, Hη)).
  - split.
    + apply nat_trans_eq.
      { apply D. }
      intros X ; cbn.
      exact (iso_inv_after_iso (pr1 η X ,, _)).
    + apply nat_trans_eq.
      { apply D. }
      intros X ; cbn.
      exact (iso_after_iso_inv (pr1 η X ,, _)).
Defined.

Definition nat_iso_to_invertible_2cell
           {C D : bicat_of_cats}
           (F G : C --> D)
  : nat_iso F G → invertible_2cell F G.
Proof.
  intros η.
  use tpair.
  - apply η.
  - apply is_nat_iso_to_is_invertible_2cell.
    apply η.
Defined.

Definition invertible_2cell_is_nat_iso
           {C D : bicat_of_cats}
           (F G : C --> D)
  : nat_iso F G ≃ invertible_2cell F G.
Proof.
  use weqpair.
  - exact (nat_iso_to_invertible_2cell F G).
  - use isweq_iso.
    + exact (invertible_2cell_to_nat_iso F G).
    + intros X.
      use subtypeEquality.
      × intro.
        apply isaprop_is_nat_iso.
      × reflexivity.
    + intros X.
      use subtypeEquality.
      × intro.
        apply isaprop_is_invertible_2cell.
      × reflexivity.
Defined.

Definition adj_equiv_to_equiv_cat
           {C D : bicat_of_cats}
           (F : C --> D)
  : left_adjoint_equivalence F → adj_equivalence_of_precats F.
Proof.
  intros A.
  use mk_adj_equivalence_of_precats.
  - exact (left_adjoint_right_adjoint A).
  - exact (left_adjoint_unit A).
  - exact (left_adjoint_counit A).
  - split.
    + intro X.
      cbn.
      pose (nat_trans_eq_pointwise (internal_triangle1 A) X) as p.
      cbn in p.
      rewrite !id_left, !id_right in p.
      exact p.
    + intro X.
      cbn.
      pose (nat_trans_eq_pointwise (internal_triangle2 A) X) as p.
      cbn in p.
      rewrite !id_left, !id_right in p.
      exact p.
  - split.
    + intro X.
      apply (invertible_2cell_to_nat_iso _ _ (left_equivalence_unit_iso A)).
    + intro X.
      apply (invertible_2cell_to_nat_iso _ _ (left_equivalence_counit_iso A)).
Defined.

Definition equiv_cat_to_adj_equiv
           {C D : bicat_of_cats}
           (F : C --> D)
  : adj_equivalence_of_precats F → left_adjoint_equivalence F.
Proof.
  intros A.
  use tpair.
  - use tpair.
    + apply A.
    + split ; cbn.
      × exact (pr1(pr1(pr2(pr1 A)))).
      × exact (pr2(pr1(pr2(pr1 A)))).
  - split ; split.
    + apply nat_trans_eq.
      { apply D. }
      intro X ; cbn.
      rewrite id_left, !id_right.
      apply (pr2(pr2(pr1 A))).
    + apply nat_trans_eq.
      { apply C. }
      intro X ; cbn.
      rewrite id_left, !id_right.
      apply (pr2(pr2(pr1 A))).
    + apply is_nat_iso_to_is_invertible_2cell.
      intro X.
      apply (pr2 A).
    + apply is_nat_iso_to_is_invertible_2cell.
      intro X.
      apply (pr2 A).
Defined.

Definition adj_equiv_is_equiv_cat
           {C D : bicat_of_cats}
           (F : C --> D)
  : left_adjoint_equivalence F ≃ adj_equivalence_of_precats F.
Proof.
  use weqpair.
  - exact (adj_equiv_to_equiv_cat F).
  - use isweq_iso.
    + exact (equiv_cat_to_adj_equiv F).
    + intros A.
      use subtypeEquality.
      × intro.
        do 2 apply isapropdirprod.
        ** apply bicat_of_cats.
        ** apply bicat_of_cats.
        ** apply isaprop_is_invertible_2cell.
        ** apply isaprop_is_invertible_2cell.
      × reflexivity.
    + intros A.
      use subtypeEquality.
      × intro.
        apply isapropdirprod ; apply impred ; intro ; apply isaprop_is_iso.
      × use total2_paths_b.
        ** reflexivity.
        ** use subtypeEquality.
           *** intro ; simpl.
               apply (@isaprop_form_adjunction (pr1 C ,, _) (pr1 D ,, _)).
           *** reflexivity.
Defined.

Definition univalent_cat_idtoiso_2_1
           {C D : univalent_category}
           (F G : bicat_of_cats⟦C,D⟧)
  : F = G ≃ invertible_2cell F G.
Proof.
  refine ((invertible_2cell_is_nat_iso F G)
            ∘ iso_is_nat_iso F G
            ∘ weqpair (@idtoiso (functor_category C D) F G) _)%weq.
  exact (pr1 (is_univalent_functor_category C D _) F G).
Defined.

Definition univalent_cat_is_univalent_2_1
  : is_univalent_2_1 bicat_of_cats.
Proof.
  intros C D f g.
  use weqhomot.
  - exact (univalent_cat_idtoiso_2_1 f g).
  - intros p.
    induction p.
    use subtypeEquality.
    + intro.
      apply isaprop_is_invertible_2cell.
    + apply nat_trans_eq.
      { apply D. }
      reflexivity.
Defined.

Definition path_univalent_cat
           (C D : bicat_of_cats)
  : C = D ≃ pr1 C = pr1 D.
Proof.
  apply path_sigma_hprop.
  simpl.
  apply isaprop_is_univalent.
Defined.

Section CatIso_To_LeftAdjEquiv.
  Context {C D : univalent_category}.
  Variable (F : C ⟶ D)
           (HF : is_catiso F).

  Local Definition cat_iso_unit
    : nat_iso
        (functor_identity C)
        (functor_composite F (inv_catiso (F ,, HF))).
  Proof.
    use tpair.
    - use mk_nat_trans.
      + intros X ; cbn.
        exact (pr1 (idtoiso (! homotinvweqweq (catiso_ob_weq (F ,, HF)) X))).
      + intros X Y f ; cbn.
        use (invmaponpathsweq (#F ,, _)).
        { apply HF. }
        cbn.
        refine (functor_comp _ _ _ @ !_).
        refine (functor_comp _ _ _ @ _).
        etrans.
        {
          apply maponpaths.
          match goal with [ |- _ (invmap ?FFF ?fff) = _ ] ⇒ apply (homotweqinvweq FFF fff) end.
        }
        rewrite !assoc.
        etrans.
        {
          refine (maponpaths (λ z, ((z · _) · _) · _) _).
          apply (!(base_paths _ _ (maponpaths_idtoiso _ _ F _ _ _))).
        }
        etrans.
        {
          refine (maponpaths (λ z, (z · _) · _) (!_)).
          apply (base_paths _ _ (idtoiso_concat _ _ _ _ _ _)).
        }
        rewrite maponpathsinv0.
        etrans.
        {
          refine (maponpaths (λ z, (pr1 (idtoiso (! z @ _)) · _) · _) _).
          match goal with [ |- _ (homotinvweqweq ?w _) = _] ⇒ apply (homotweqinvweqweq w) end.
        }
        rewrite pathsinv0l ; cbn.
        rewrite id_left.
        apply maponpaths.
        etrans.
        {
          repeat apply maponpaths.
          match goal with [ |- (homotweqinvweq ?w _) = _] ⇒ apply (! homotweqinvweqweq w Y) end.
        }
        rewrite <- maponpathsinv0.
        apply (base_paths _ _ (maponpaths_idtoiso _ _ F _ _ _)).
    - intros X.
      apply (idtoiso (! homotinvweqweq (catiso_ob_weq (F ,, HF)) X)).
  Defined.

  Local Definition cat_iso_counit
    : nat_iso
        (functor_composite (inv_catiso (F ,, HF)) F)
        (functor_identity (pr1 (pr1 D))).
  Proof.
    use tpair.
    - use mk_nat_trans.
      + intros X ; cbn.
        exact (pr1 (idtoiso (homotweqinvweq (catiso_ob_weq (F ,, HF)) X))).
      + intros X Y f ; cbn.
        etrans.
        {
          apply maponpaths_2.
          match goal with [ |- _ (invmap ?FFF ?fff) = _ ] ⇒ apply (homotweqinvweq FFF fff) end.
        }
        rewrite <- !assoc.
        etrans.
        {
          refine (maponpaths (λ z, _ · (_ · z)) _).
          apply (base_paths _ _ (!(idtoiso_concat _ _ _ _ _ _))).
        }
        rewrite pathsinv0l ; cbn.
        rewrite id_right.
        reflexivity.
    - intros X.
      apply (idtoiso (homotweqinvweq (catiso_ob_weq (F ,, HF)) X)).
  Defined.

  Definition is_catiso_to_left_adjoint_equivalence
    : @left_adjoint_equivalence bicat_of_cats _ _ F.
  Proof.
    use equiv_to_adjequiv.
    use tpair.
    - use tpair.
      + exact (inv_catiso (F ,, HF)).
      + split.
        × apply cat_iso_unit.
        × apply cat_iso_counit.
    - split.
      + use tpair ; try split.
        × apply (nat_iso_inv cat_iso_unit).
        × apply nat_trans_eq.
          { apply C. }
          intro X ; cbn.
          rewrite idtoiso_inv ; cbn ; unfold precomp_with.
          rewrite id_right.
          apply iso_after_iso_inv.
        × apply nat_trans_eq.
          { apply C. }
          intro X ; cbn.
          rewrite idtoiso_inv ; cbn ; unfold precomp_with.
          rewrite id_right.
          apply iso_inv_after_iso.
      + use tpair ; try split.
        × apply (nat_iso_inv cat_iso_counit).
        × apply nat_trans_eq.
          { apply D. }
          intro X ; cbn.
          apply iso_inv_after_iso.
        × apply nat_trans_eq.
          { apply D. }
          intro X ; cbn.
          apply iso_after_iso_inv.
  Qed.
End CatIso_To_LeftAdjEquiv.

Definition left_adjoint_equivalence_to_is_catiso
           {C D : bicat_of_cats}
           (L : (pr1 C) ⟶ (pr1 D))
  : @left_adjoint_equivalence bicat_of_cats _ _ L → is_catiso L.
Proof.
  intros HF.
  pose (R := pr1 (left_adjoint_right_adjoint HF)).
  pose (η := left_adjoint_unit HF).
  pose (ηinv := (left_equivalence_unit_iso HF)^-1).
  pose (ε := left_adjoint_counit HF).
  pose (εinv := (left_equivalence_counit_iso HF)^-1).
  assert (ηηinv := nat_trans_eq_pointwise
                     (pr1(pr2(pr2 (left_equivalence_unit_iso HF))))).
  assert (ηinvη := nat_trans_eq_pointwise
                     (pr2(pr2(pr2 (left_equivalence_unit_iso HF))))).
  assert (εεinv := nat_trans_eq_pointwise
                     (pr1(pr2(pr2 (left_equivalence_counit_iso HF))))).
  assert (εinvε := nat_trans_eq_pointwise
                     (pr2(pr2(pr2 (left_equivalence_counit_iso HF))))).
  assert (LηεL := nat_trans_eq_pointwise (internal_triangle1 HF)).
  assert (ηRRε := nat_trans_eq_pointwise (internal_triangle2 HF)).
  cbn in ×.
  use tpair.
  - intros X Y.
    use isweq_iso.
    + intros f.
      exact (η X · #R f · ηinv Y).
    + intros f ; cbn.
      etrans.
      {
        apply maponpaths_2.
        exact (!(pr2 η X Y f)).
      }
      rewrite <- assoc.
      refine (maponpaths (λ z, _ · z) (ηηinv Y) @ _).
      apply id_right.
    + intros f ; cbn.
      rewrite !functor_comp.
      assert (#L (ηinv Y) = ε (L Y)) as X0.
      {
        specialize (LηεL Y).
        rewrite !id_left, !id_right in LηεL.
        refine (!(id_right _) @ _).
        refine (maponpaths (λ z, _ · z) (!LηεL) @ _).
        rewrite assoc.
        rewrite <- functor_comp.
        refine (maponpaths (λ z, # L z · _) (ηinvη Y) @ _).
        rewrite functor_id, id_left.
        reflexivity.
      }
      etrans.
      {
        apply maponpaths.
        exact X0.
      }
      rewrite <- assoc.
      refine (maponpaths _ (nat_trans_ax ε (L X) (L Y) f) @ _).
      rewrite assoc.
      specialize (LηεL X).
      rewrite !id_left, !id_right in LηεL.
      etrans.
      {
        apply maponpaths_2.
        exact LηεL.
      }
      apply id_left.
  - cbn.
    use isweq_iso.
    + apply R.
    + intros X ; cbn.
      apply isotoid.
      × apply C.
      × use tpair.
        ** exact (ηinv X).
        ** use is_iso_qinv ; try split.
           *** exact (η X).
           *** exact (ηinvη X).
           *** exact (ηηinv X).
    + intros Y ; cbn.
      apply isotoid.
      × apply D.
      × use tpair.
        ** exact (ε Y).
        ** use is_iso_qinv ; try split.
           *** exact (εinv Y).
           *** exact (εεinv Y).
           *** exact (εinvε Y).
Qed.

Definition is_catiso_left_adjoint_equivalence
           {C D : univalent_category}
           (F : C ⟶ D)
  : is_catiso F ≃ @left_adjoint_equivalence bicat_of_cats C D F.
Proof.
  use weqimplimpl.
  - exact (is_catiso_to_left_adjoint_equivalence F).
  - exact (left_adjoint_equivalence_to_is_catiso F).
  - apply isaprop_is_catiso.
  - apply invproofirrelevance.
    intros A₁ A₂.
    apply unique_internal_adjoint_equivalence.
    apply univalent_cat_is_univalent_2_1.
Defined.

Definition cat_iso_to_adjequiv
           (C D : bicat_of_cats)
  : catiso (pr1 C) (pr1 D) ≃ adjoint_equivalence C D.
Proof.
  use weqfibtototal.
  intros.
  apply is_catiso_left_adjoint_equivalence.
Defined.

Definition idtoiso_2_0_univalent_cat
           (C D : bicat_of_cats)
  : C = D ≃ adjoint_equivalence C D
  := ((cat_iso_to_adjequiv C D)
        ∘ catiso_is_path_precat (pr1 C) (pr1 D) (pr2(pr2 D))
        ∘ path_univalent_cat C D)%weq.

Definition univalent_cat_is_univalent_2_0
  : is_univalent_2_0 bicat_of_cats.
Proof.
  intros C D.
  use weqhomot.
  - exact (idtoiso_2_0_univalent_cat C D).
  - intro p.
    induction p.
    apply path_internal_adjoint_equivalence.
    + apply univalent_cat_is_univalent_2_1.
    + reflexivity.
Defined.