Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Invertible_2cells.

Local Open Scope bicategory_scope.
Local Open Scope cat.

Section Internal_Adjunction.
  Context {B : bicat}.

  Definition left_adjoint_data
             {a b : B}
             (f : a --> b)
    : UU
    := ∑ (g : b --> a),
       identity a ==> f · g
       ×
       g · f ==> identity b.

  Definition left_adjoint_right_adjoint
             {a b : B}
             {f : a --> b}
             (αd : left_adjoint_data f)
    : b --> a
    := pr1 αd.

  Definition left_adjoint_unit
             {a b : B}
             {f : a --> b}
             (αd : left_adjoint_data f)
    : identity a ==> f · left_adjoint_right_adjoint αd
    := pr12 αd.

  Definition left_adjoint_counit
             {a b : B}
             {f : a --> b}
             (αd : left_adjoint_data f)
    : left_adjoint_right_adjoint αd · f ==> identity b
    := pr22 αd.

  Definition left_adjoint_axioms
             {a b : B}
             {f : a --> b}
             (αd : left_adjoint_data f)
    : UU
    := let g := left_adjoint_right_adjoint αd in
       let η := left_adjoint_unit αd in
       let ε := left_adjoint_counit αd in
       linvunitor f • (η ▹ f) • rassociator _ _ _ • (f ◃ ε) • runitor f = id2 f
       ×
       rinvunitor g • (g ◃ η) • lassociator _ _ _ • (ε ▹ g) • lunitor g = id2 g.

  Definition left_adjoint
             {a b : B}
             (f : a --> b)
    : UU
    := ∑ (αd : left_adjoint_data f), left_adjoint_axioms αd.

  Coercion data_of_left_adjoint
           {a b : B}
           {f : a --> b}
           (α : left_adjoint f)
    : left_adjoint_data f
    := pr1 α.

  Coercion axioms_of_left_adjoint
           {a b : B}
           {f : a --> b}
           (α : left_adjoint f)
    : left_adjoint_axioms α
    := pr2 α.

  Definition internal_right_adj_data
             {a b : B}
             (g : b --> a)
    : UU
    := ∑ (f : a --> b),
       identity a ==> f · g
       ×
       g · f ==> identity b.

  Definition internal_right_adj_left_adjoint
             {a b : B}
             {g : b --> a}
             (αd : internal_right_adj_data g)
    : a --> b
    := pr1 αd.

  Definition internal_right_adj_unit
             {a b : B}
             {g : b --> a}
             (αd : internal_right_adj_data g)
    : identity a ==> internal_right_adj_left_adjoint αd · g
    := pr12 αd.

  Definition internal_right_adj_counit
             {a b : B}
             {g : b --> a}
             (αd : internal_right_adj_data g)
    : g · internal_right_adj_left_adjoint αd ==> identity b
    := pr22 αd.

  Definition internal_right_adj_axioms
             {a b : B}
             {g : b --> a}
             (αd : internal_right_adj_data g)
    : UU
    := let f := internal_right_adj_left_adjoint αd in
       let η := internal_right_adj_unit αd in
       let ε := internal_right_adj_counit αd in
       linvunitor f • (η ▹ f) • rassociator _ _ _ • (f ◃ ε) • runitor f = id2 f
       ×
       rinvunitor g • (g ◃ η) • lassociator _ _ _ • (ε ▹ g) • lunitor g = id2 g.

  Definition internal_right_adj
             {a b : B}
             (g : b --> a)
    : UU
    := ∑ (αd : internal_right_adj_data g), internal_right_adj_axioms αd.

  Coercion data_of_internal_right_adj
           {a b : B}
           {g : b --> a}
           (α : internal_right_adj g)
    : internal_right_adj_data g
    := pr1 α.

  Coercion axioms_of_internal_right_adj
           {a b : B}
           {g : b --> a}
           (α : internal_right_adj g)
    : internal_right_adj_axioms α
    := pr2 α.

  Definition left_equivalence_axioms
             {a b : B}
             {f : a --> b}
             (αd : left_adjoint_data f)
    : UU
    := is_invertible_2cell (left_adjoint_unit αd)
       ×
       is_invertible_2cell (left_adjoint_counit αd).

  Definition left_equivalence
             {a b : B}
             (f : a --> b)
    :UU
    := ∑ (αd : left_adjoint_data f),
       left_equivalence_axioms αd.

  Coercion data_of_left_equivalence
           {a b : B}
           {f : a --> b}
           (αe : left_equivalence f)
    : left_adjoint_data f
    := pr1 αe.

  Coercion axioms_of_left_equivalence
           {a b : B}
           {f : a --> b}
           (αe : left_equivalence f)
    : left_equivalence_axioms αe
    := pr2 αe.

  Definition left_adjoint_equivalence
             {a b : B}
             (f : a --> b)
    : UU
    := ∑ (αd : left_adjoint_data f),
       left_adjoint_axioms αd
       ×
       left_equivalence_axioms αd.

  Coercion left_adjoint_of_left_adjoint_equivalence
           {a b : B}
           {f : a --> b}
           (αe : left_adjoint_equivalence f)
    : left_adjoint f
    := (pr1 αe,, pr12 αe).

  Coercion left_equivalence_of_left_adjoint_equivalence
           {a b : B}
           {f : a --> b}
           (αe : left_adjoint_equivalence f)
    : left_equivalence f
    := (pr1 αe,, pr22 αe).

  Definition left_equivalence_unit_iso
             {a b : B}
             {f : a --> b}
             (αe : left_equivalence f)
    : invertible_2cell (identity a) (f · left_adjoint_right_adjoint αe).
  Show proof.

  Definition left_equivalence_counit_iso
             {a b : B}
             {f : a --> b}
             (αe : left_equivalence f)
    : invertible_2cell (left_adjoint_right_adjoint αe · f) (identity b).
  Show proof.

  Definition adjunction (a b : B) : UU
    := ∑ (f : a --> b), left_adjoint f.

  Coercion arrow_of_adjunction
           {a b : B}
           (f : adjunction a b)
    : a --> b
    := pr1 f.

  Coercion left_adjoint_of_adjunction
           {a b : B}
           (f : adjunction a b)
    : left_adjoint f
    := pr2 f.

  Definition adjoint_equivalence
             (a b : B)
    : UU
    := ∑ (f : a --> b), left_adjoint_equivalence f.

  Coercion adjunction_of_adjoint_equivalence
           {a b : B}
           (f : adjoint_equivalence a b)
    : adjunction a b
    := (pr1 f,,left_adjoint_of_left_adjoint_equivalence (pr2 f)).

  Coercion left_adjoint_equivalence_of_adjoint_equivalence
           {a b : B}
           (f : adjoint_equivalence a b)
    : left_adjoint_equivalence f
    := pr2 f.

  Definition internal_right_adjoint
             {a b : B}
             (f : adjunction a b)
    : b --> a
    := left_adjoint_right_adjoint f.

  Definition internal_triangle1
             {a b : B}
             {f : a --> b}
             {adj : left_adjoint_data f}
             (L : left_adjoint_axioms adj)
    : linvunitor f
      • (left_adjoint_unit adj ▹ f)
      • rassociator _ _ _
      • (f ◃ left_adjoint_counit adj)
      • runitor f
      =
      id2 f
    := pr1 L.

  Definition internal_triangle2
             {a b : B}
             {f : a --> b}
             {adj : left_adjoint_data f}
             (L : left_adjoint_axioms adj)
             (g := left_adjoint_right_adjoint adj)
    : rinvunitor g
      • (g ◃ left_adjoint_unit adj)
      • lassociator _ _ _
      • (left_adjoint_counit adj ▹ g)
      • lunitor g
      =
      id2 g
    := pr2 L.

  Definition make_adjoint_equivalence
             {a b : B}
             (f : a --> b)
             (g : b --> a)
             (η : identity _ ==> g ∘ f)
             (ε : f ∘ g ==> identity _)
             (triangle1 : linvunitor f
                          • (η ▹ f)
                          • rassociator _ _ _
                          • (f ◃ ε)
                          • runitor f
                          =
                          id2 f)
             (triangle2 : rinvunitor g
                          • (g ◃ η)
                          • lassociator _ _ _
                          • (ε ▹ g)
                          • lunitor g
                          =
                          id2 g)
             (η_iso : is_invertible_2cell η)
             (ε_iso : is_invertible_2cell ε)
    : adjoint_equivalence a b
    := f ,, ((g ,, (η ,, ε)) ,, ((triangle1 ,, triangle2) ,, (η_iso ,, ε_iso))).
End Internal_Adjunction.