(** * Classify the path space of adjunctions *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import Functor.Composition.Core Functor.Identity.
Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths.
Require Import Types Trunc.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.
Local Open Scope natural_transformation_scope.

Section path_adjunction.
  Context `{Funext}.

  Variables C D : PreCategory.
  Variable F : Functor C D.
  Variable G : Functor D C.

  Notation adjunction_sig :=
    { eta : NaturalTransformation 1 (G o F)
    | { eps : NaturalTransformation (F o G) 1
      | { equ1 : forall Y : C, (eps (F Y) o F _1 (eta Y))%morphism = 1%morphism
        | forall X : D, (G _1 (eps X) o eta (G X))%morphism = 1%morphism }}}.

  (** ** Equivalence between record and nested sigma for unit+counit adjunctions *)
  Lemma equiv_sig_adjunction
  : adjunction_sig <~> (F -| G).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
{eta : NaturalTransformation 1 (G o F) &
{eps : NaturalTransformation (F o G) 1 &
{_ : forall Y : C, eps (F _0 Y)%object o F _1 (eta Y) = 1 &
forall X : D, G _1 (eps X) o eta (G _0 X)%object = 1}}} <~> 
F -| G
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
{eta : NaturalTransformation 1 (G o F) &
{eps : NaturalTransformation (F o G) 1 &
{_ : forall Y : C, eps (F _0 Y)%object o F _1 (eta Y) = 1 &
forall X : D, G _1 (eps X) o eta (G _0 X)%object = 1}}} <~> 
F -| G
    issig.
  Defined.

  (** ** Adjunctions are an hSet *)
  #[export] Instance trunc_adjunction : IsHSet (F -| G).
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
IsHSet (F -| G)
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
IsHSet (F -| G)
    eapply istrunc_equiv_istrunc; [ exact equiv_sig_adjunction | ].
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
IsHSet
  {eta : NaturalTransformation 1 (G o F) &
  {eps : NaturalTransformation (F o G) 1 &
  {_ : forall Y : C, eps (F _0 Y)%object o F _1 (eta Y) = 1 &
  forall X : D, G _1 (eps X) o eta (G _0 X)%object = 1}}}
    typeclasses eauto.
  Qed.

  (** ** Equality of adjunctions follows from equality of unit+counit *)
  Lemma path_adjunction' (A A' : F -| G)
  : unit A = unit A'
    -> counit A = counit A'
    -> A = A'.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
unit A = unit A' -> counit A = counit A' -> A = A'
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
unit A = unit A' -> counit A = counit A' -> A = A'
    intros.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
X: unit A = unit A'
X0: counit A = counit A'
A = A'
    destruct A, A'; simpl in *.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
unit: NaturalTransformation 1 (G o F)
counit: NaturalTransformation (F o G) 1
unit_counit_equation_1: forall Y : C, counit (F _0 Y)%object o F _1 (unit Y) = 1
unit_counit_equation_2: forall X1 : D, G _1 (counit X1) o unit (G _0 X1)%object = 1
unit0: NaturalTransformation 1 (G o F)
counit0: NaturalTransformation (F o G) 1
unit_counit_equation_0: forall Y : C, counit0 (F _0 Y)%object o F _1 (unit0 Y) = 1
unit_counit_equation_3: forall X1 : D, G _1 (counit0 X1) o unit0 (G _0 X1)%object = 1
X: unit = unit0
X0: counit = counit0
{|
  unit := unit;
  counit := counit;
  unit_counit_equation_1 := unit_counit_equation_1;
  unit_counit_equation_2 := unit_counit_equation_2
|} =
{|
  unit := unit0;
  counit := counit0;
  unit_counit_equation_1 := unit_counit_equation_0;
  unit_counit_equation_2 := unit_counit_equation_3
|}
    path_induction.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
unit: NaturalTransformation 1 (G o F)
counit: NaturalTransformation (F o G) 1
unit_counit_equation_1: forall Y : C, counit (F _0 Y)%object o F _1 (unit Y) = 1
unit_counit_equation_2: forall X : D, G _1 (counit X) o unit (G _0 X)%object = 1
unit_counit_equation_0: forall Y : C, counit (F _0 Y)%object o F _1 (unit Y) = 1
unit_counit_equation_3: forall X : D, G _1 (counit X) o unit (G _0 X)%object = 1
{|
  unit := unit;
  counit := counit;
  unit_counit_equation_1 := unit_counit_equation_1;
  unit_counit_equation_2 := unit_counit_equation_2
|} =
{|
  unit := unit;
  counit := counit;
  unit_counit_equation_1 := unit_counit_equation_0;
  unit_counit_equation_2 := unit_counit_equation_3
|}
    f_ap;
      exact (center _).
  Qed.

  (** ** Equality of adjunctions follows from equality of action of unit+counit on objects *)
  Lemma path_adjunction (A A' : F -| G)
  : components_of (unit A) == components_of (unit A')
    -> components_of (counit A) == components_of (counit A')
    -> A = A'.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
unit A == unit A' -> counit A == counit A' -> A = A'
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
unit A == unit A' -> counit A == counit A' -> A = A'
    intros.
H: Funext
C, D: PreCategory
F: Functor C D
G: Functor D C
A, A': F -| G
X: unit A == unit A'
X0: counit A == counit A'
A = A'
    apply path_adjunction';
    apply path_natural_transformation;
    assumption.
  Qed.

  (** In fact, it suffices to show that either the units are equal, or
      the counits are equal, by the UMP of the (co)unit.  And if we
      are working in a [Category], rather than a [PreCategory], then
      [Adjunction] is, in fact, an hProp, because the (co)unit is
      unique up to unique isomorphism.

      TODO: Formalize this. *)
End path_adjunction.

Ltac path_adjunction :=
  repeat match goal with
           | _ => intro
           | _ => reflexivity
           | _ => apply path_adjunction; simpl
         end.