Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
(** * Associativity of adjunction composition *)

[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Require Import Adjoint.Composition.Core Adjoint.Core.
Require Adjoint.Composition.LawsTactic.
Require Import Types.Sigma Types.Prod.

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

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.

  
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))

  
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))

    
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.