(** * Associativity of adjunction composition *)
Require Import Category.Core Functor.Core.
Require Import Adjoint.Composition.Core Adjoint.Core.
Require Adjoint.Composition.LawsTactic.
Require Import Types.Sigma Types.Prod.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope adjunction_scope.
Local Open Scope morphism_scope.

Section composition_lemmas.
  Local Notation AdjunctionWithFunctors C D :=
    { fg : Functor C D * Functor D C
    | fst fg -| snd fg }.

  Context `{H0 : Funext}.

  Variables B C D E : PreCategory.

  Variable F : Functor B C.
  Variable F' : Functor C B.
  Variable G : Functor C D.
  Variable G' : Functor D C.
  Variable H : Functor D E.
  Variable H' : Functor E D.

  Variable AF : F -| F'.
  Variable AG : G -| G'.
  Variable AH : H -| H'.

  Local Open Scope adjunction_scope.

  Lemma associativity
  : ((_, _); (AH o AG) o AF) = ((_, _); AH o (AG o AF)) :> AdjunctionWithFunctors B E.
H0: Funext
B, C, D, E: PreCategory
F: Functor B C
F': Functor C B
G: Functor C D
G': Functor D C
H: Functor D E
H': Functor E D
AF: F -| F'
AG: G -| G'
AH: H -| H'
((Functor.Composition.Core.compose (Functor.Composition.Core.compose H G) F,
 Functor.Composition.Core.compose F' (Functor.Composition.Core.compose G' H'));
AH o AG o AF) =
((Functor.Composition.Core.compose H (Functor.Composition.Core.compose G F),
 Functor.Composition.Core.compose (Functor.Composition.Core.compose F' G') H');
AH o (AG o AF))
  Proof.
H0: Funext
B, C, D, E: PreCategory
F: Functor B C
F': Functor C B
G: Functor C D
G': Functor D C
H: Functor D E
H': Functor E D
AF: F -| F'
AG: G -| G'
AH: H -| H'
((Functor.Composition.Core.compose (Functor.Composition.Core.compose H G) F,
 Functor.Composition.Core.compose F' (Functor.Composition.Core.compose G' H'));
AH o AG o AF) =
((Functor.Composition.Core.compose H (Functor.Composition.Core.compose G F),
 Functor.Composition.Core.compose (Functor.Composition.Core.compose F' G') H');
AH o (AG o AF))
    apply path_sigma_uncurried; simpl.
H0: Funext
B, C, D, E: PreCategory
F: Functor B C
F': Functor C B
G: Functor C D
G': Functor D C
H: Functor D E
H': Functor E D
AF: F -| F'
AG: G -| G'
AH: H -| H'
{p
: (Functor.Composition.Core.compose (Functor.Composition.Core.compose H G) F,
  Functor.Composition.Core.compose F'
    (Functor.Composition.Core.compose G' H')) =
  (Functor.Composition.Core.compose H (Functor.Composition.Core.compose G F),
  Functor.Composition.Core.compose (Functor.Composition.Core.compose F' G')
    H')
&
transport (fun fg : Functor B E * Functor E B => fst fg -| snd fg) p
  (AH o AG o AF) =
AH o (AG o AF)}
    (exists (path_prod'
               (Functor.Composition.Laws.associativity _ _ _)
               (symmetry _ _ (Functor.Composition.Laws.associativity _ _ _))));
      Adjoint.Composition.LawsTactic.law_t.
  Qed.
End composition_lemmas.

#[export]
Hint Resolve associativity : category.