(** * Classify the path space of adjunctions *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Composition.Core Functor.Identity.
Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths.
Require Import Types Trunc.
Require Import Basics.Tactics.

Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.

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 X : D,
G _1 (counit X)
o unit (G _0 X)%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 X : D,
G _1 (counit0 X)
o unit0 (G _0 X)%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.