(** * Laws about composition of functors *)
Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Identity.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Functor.Paths.
Require Import Basics.PathGroupoids Basics.Tactics.

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

Local Open Scope morphism_scope.

Section identity_lemmas.
  Context `{Funext}.

  Variables C D : PreCategory.

  Local Open Scope functor_scope.

  (** ** left identity : [1 ∘ F = F] *)
  (** If we had that [match (p : a = b) in (_ = y) return (a = y) with idpath => idpath end ≡ p] (a form of eta for paths), this would be judgemental. *)
  Lemma left_identity (F : Functor C D) : 1 o F = F.
H: Funext
C, D: PreCategory
F: Functor C D
1 o F = F
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
1 o F = F
    by path_functor.
  Defined.

  (** ** right identity : [F ∘ 1 = F] *)
  Lemma right_identity (F : Functor C D) : F o 1 = F.
H: Funext
C, D: PreCategory
F: Functor C D
F o 1 = F
  Proof.
H: Funext
C, D: PreCategory
F: Functor C D
F o 1 = F
    by path_functor.
  Defined.

  (** ** Action of left and right identity laws on objects *)
  Definition left_identity_fst F
  : ap object_of (left_identity F) = idpath
    := @path_functor_uncurried_fst _ _ _ (1 o F) F 1 1.

  Definition right_identity_fst F
  : ap object_of (right_identity F) = idpath
    := @path_functor_uncurried_fst _ _ _ (F o 1) F 1 1.
End identity_lemmas.

#[export]
Hint Rewrite @left_identity @right_identity : category.
#[export]
Hint Rewrite @left_identity @right_identity : functor.
#[export]
Hint Immediate left_identity right_identity : category functor.

Section composition_lemmas.
  Context `{fs : Funext}.

  Variables B C D E : PreCategory.

  Local Open Scope functor_scope.

  (** ** associativity : [(H ∘ G) ∘ F = H ∘ (G ∘ F)] *)
  Lemma associativity
        (F : Functor B C) (G : Functor C D) (H : Functor D E)
  : (H o G) o F = H o (G o F).
fs: Funext
B, C, D, E: PreCategory
F: Functor B C
G: Functor C D
H: Functor D E
H o G o F = H o (G o F)
  Proof.
fs: Funext
B, C, D, E: PreCategory
F: Functor B C
G: Functor C D
H: Functor D E
H o G o F = H o (G o F)
    by path_functor.
  Defined.

  (** ** Action of associativity on objects *)
  Definition associativity_fst F G H
  : ap object_of (associativity F G H) = idpath
    := @path_functor_uncurried_fst _ _ _ ((H o G) o F) (H o (G o F)) 1%path 1%path.
End composition_lemmas.

#[export]
Hint Resolve associativity : category functor.

Section coherence.
  Context `{fs : Funext}.

  Local Open Scope path_scope.
  Local Open Scope functor_scope.

  Local Ltac coherence_t :=
    repeat match goal with
             | [ |- _ = _ :> (_ = _ :> Functor _ _) ] => apply path_path_functor_uncurried
             | _ => reflexivity
             | _ => progress rewrite ?ap_pp, ?concat_1p, ?concat_p1
             | _ => progress rewrite ?associativity_fst, ?left_identity_fst, ?right_identity_fst
             | _ => progress push_ap_object_of
           end.

  (** ** coherence triangle *)
  (** The following triangle is coherent
<<
      G ∘ (1 ∘ F) === (G ∘ 1) ∘ F
            \\           //
             \\         //
              \\       //
               \\     //
                \\   //
                 \\ //
                 G ∘ F
>>
*)
  Lemma triangle C D E (F : Functor C D) (G : Functor D E)
  : (associativity F 1 G @ ap (compose G) (left_identity F))
    = (ap (fun G' : Functor D E => G' o F) (right_identity G)).
fs: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D E
associativity F 1 G @ ap (compose G) (left_identity F) =
ap (fun G' : Functor D E => G' o F) (right_identity G)
  Proof.
fs: Funext
C, D, E: PreCategory
F: Functor C D
G: Functor D E
associativity F 1 G @ ap (compose G) (left_identity F) =
ap (fun G' : Functor D E => G' o F) (right_identity G)
    coherence_t.
  Qed.

  (** ** coherence pentagon *)
  (** The following pentagon is coherent
<<
                  K ∘ (H ∘ (G ∘ F))
                  //             \\
                 //               \\
                //                 \\
               //                   \\
              //                     \\
      (K ∘ H) ∘ (G ∘ F)        K ∘ ((H ∘ G) ∘ F)
              ||                      ||
              ||                      ||
              ||                      ||
              ||                      ||
              ||                      ||
      ((K ∘ H) ∘ G) ∘ F ====== (K ∘ (H ∘ G)) ∘ F
>>
*)
  Lemma pentagon A B C D E
        (F : Functor A B) (G : Functor B C) (H : Functor C D) (K : Functor D E)
  : (associativity F G (K o H) @ associativity (G o F) H K)
    = (ap (fun KHG => KHG o F) (associativity G H K) @ associativity F (H o G) K @ ap (compose K) (associativity F G H)).
fs: Funext
A, B, C, D, E: PreCategory
F: Functor A B
G: Functor B C
H: Functor C D
K: Functor D E
associativity F G (K o H) @ associativity (G o F) H K =
(ap (fun KHG : Functor B E => KHG o F)
   (associativity G H K) @ associativity F (H o G) K) @
ap (compose K) (associativity F G H)
  Proof.
fs: Funext
A, B, C, D, E: PreCategory
F: Functor A B
G: Functor B C
H: Functor C D
K: Functor D E
associativity F G (K o H) @ associativity (G o F) H K =
(ap (fun KHG : Functor B E => KHG o F)
   (associativity G H K) @ associativity F (H o G) K) @
ap (compose K) (associativity F G H)
    coherence_t.
  Qed.
End coherence.

Arguments associativity : simpl never.
Arguments left_identity : simpl never.
Arguments right_identity : simpl never.