(** * Natural isomorphisms *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.
Require Import NaturalTransformation.Composition.Core.
Require Import Functor.Composition.Core.
Require Import Category.Morphisms.
Require Import FunctorCategory.Core.
Require Import NaturalTransformation.Paths.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.
Local Open Scope natural_transformation_scope.
Local Open Scope morphism_scope.
Local Ltac iso_whisker_t :=
  path_natural_transformation;
  try rewrite <- composition_of, <- identity_of;
  try f_ap;
  match goal with
    | [ H : IsIsomorphism _
        |- context[components_of ?T0 ?x o components_of ?T1 ?x] ]
      => change (T0 x o T1 x)
         with (components_of ((T0 : morphism (_ -> _) _ _)
                                o (T1 : morphism (_ -> _) _ _))%morphism
                             x);
        progress rewrite ?(@left_inverse _ _ _ _ H), ?(@right_inverse _ _ _ _ H)
  end;
  reflexivity.

Section composition.
  Context `{Funext}.

  (** ** Natural isomorphism respects composition *)
  #[export] Instance isisomorphism_compose
         `(T' : @NaturalTransformation C D F' F'')
         `(T : @NaturalTransformation C D F F')
         `{@IsIsomorphism (C -> D) F' F'' T'}
         `{@IsIsomorphism (C -> D) F F' T}
  : @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation
    := @isisomorphism_compose (C -> D) _ _ T' _ _ T _.

  (** ** Left whiskering preserves natural isomorphisms *)
  #[export] Instance iso_whisker_l C D E
         (F : Functor D E)
         (G G' : Functor C D)
         (T : NaturalTransformation G G')
         `{@IsIsomorphism (C -> D) G G' T}
  : @IsIsomorphism (C -> E) (F o G)%functor (F o G')%functor (whisker_l F T).
H: Funext
C, D, E: PreCategory
F: Functor D E
G, G': Functor C D
T: NaturalTransformation G G'
H0: IsIsomorphism T
IsIsomorphism (F oL T)
  Proof.
H: Funext
C, D, E: PreCategory
F: Functor D E
G, G': Functor C D
T: NaturalTransformation G G'
H0: IsIsomorphism T
IsIsomorphism (F oL T)
    exists (whisker_l F (T : morphism (_ -> _) _ _)^-1);
    abstract iso_whisker_t.
  Defined.

  (** ** Right whiskering preserves natural isomorphisms *)
  #[export] Instance iso_whisker_r C D E
         (F F' : Functor D E)
         (T : NaturalTransformation F F')
         (G : Functor C D)
         `{@IsIsomorphism (D -> E) F F' T}
  : @IsIsomorphism (C -> E) (F o G)%functor (F' o G)%functor (whisker_r T G).
H: Funext
C, D, E: PreCategory
F, F': Functor D E
T: NaturalTransformation F F'
G: Functor C D
H0: IsIsomorphism T
IsIsomorphism (T oR G)
  Proof.
H: Funext
C, D, E: PreCategory
F, F': Functor D E
T: NaturalTransformation F F'
G: Functor C D
H0: IsIsomorphism T
IsIsomorphism (T oR G)
    exists (whisker_r (T : morphism (_ -> _) _ _)^-1 G);
    abstract iso_whisker_t.
  Defined.

  (** ** action of [idtoiso] on objects *)
  Definition idtoiso_components_of C D
             (F G : Functor C D)
             (T' : F = G)
             x
  : (Category.Morphisms.idtoiso (_ -> _) T' : morphism _ _ _) x
    = Category.Morphisms.idtoiso _ (ap10 (ap object_of T') x).
H: Funext
C, D: PreCategory
F, G: Functor C D
T': F = G
x: C
(idtoiso (C -> D) T' : morphism (C -> D) F G) x =
idtoiso D (ap10 (ap object_of T') x)
  Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
T': F = G
x: C
(idtoiso (C -> D) T' : morphism (C -> D) F G) x =
idtoiso D (ap10 (ap object_of T') x)
    destruct T'.
H: Funext
C, D: PreCategory
F: Functor C D
x: C
idtoiso (C -> D) 1 x = idtoiso D (ap10 (ap object_of 1) x)
    reflexivity.
  Defined.

  (** ** [idtoiso] respects composition *)
  Definition idtoiso_compose C D
         (F F' F'' : Functor C D)
         (T' : F' = F'')
         (T : F = F')
  : ((Category.Morphisms.idtoiso (_ -> _) T' : morphism _ _ _)
       o (Category.Morphisms.idtoiso (_ -> _) T : morphism _ _ _))%natural_transformation
    = (Category.Morphisms.idtoiso (_ -> _) (T @ T')%path : morphism _ _ _).
H: Funext
C, D: PreCategory
F, F', F'': Functor C D
T': F' = F''
T: F = F'
((idtoiso (C -> D) T' : morphism (C -> D) F' F'')
 o (idtoiso (C -> D) T : morphism (C -> D) F F'))%natural_transformation =
(idtoiso (C -> D) (T @ T') : morphism (C -> D) F F'')
  Proof.
H: Funext
C, D: PreCategory
F, F', F'': Functor C D
T': F' = F''
T: F = F'
((idtoiso (C -> D) T' : morphism (C -> D) F' F'')
 o (idtoiso (C -> D) T : morphism (C -> D) F F'))%natural_transformation =
(idtoiso (C -> D) (T @ T') : morphism (C -> D) F F'')
    path_natural_transformation; path_induction; simpl; auto with morphism.
  Defined.

  (** ** left whiskering respects [idtoiso] *)
  Definition idtoiso_whisker_l C D E
         (F : Functor D E)
         (G G' : Functor C D)
         (T : G = G')
  : whisker_l F (Category.Morphisms.idtoiso (_ -> _) T : morphism _ _ _)
    = (Category.Morphisms.idtoiso (_ -> _) (ap _ T) : morphism _ _ _).
H: Funext
C, D, E: PreCategory
F: Functor D E
G, G': Functor C D
T: G = G'
F oL (idtoiso (C -> D) T : morphism (C -> D) G G') =
(idtoiso (C -> E) (ap (compose F) T)
 :
 morphism (C -> E) (F o G)%functor (F o G')%functor)
  Proof.
H: Funext
C, D, E: PreCategory
F: Functor D E
G, G': Functor C D
T: G = G'
F oL (idtoiso (C -> D) T : morphism (C -> D) G G') =
(idtoiso (C -> E) (ap (compose F) T)
 :
 morphism (C -> E) (F o G)%functor (F o G')%functor)
    path_natural_transformation; path_induction; simpl; auto with functor.
  Defined.

  (** ** right whiskering respects [idtoiso] *)
  Definition idtoiso_whisker_r C D E
         (F F' : Functor D E)
         (T : F = F')
         (G : Functor C D)
  : whisker_r (Category.Morphisms.idtoiso (_ -> _) T : morphism _ _ _) G
    = (Category.Morphisms.idtoiso (_ -> _) (ap (fun _ => _ o _)%functor T) : morphism _ _ _).
H: Funext
C, D, E: PreCategory
F, F': Functor D E
T: F = F'
G: Functor C D
(idtoiso (D -> E) T : morphism (D -> E) F F') oR G =
(idtoiso (C -> E) (ap (fun H0 : Functor D E => (H0 o G)%functor) T)
 :
 morphism (C -> E) (F o G)%functor (F' o G)%functor)
  Proof.
H: Funext
C, D, E: PreCategory
F, F': Functor D E
T: F = F'
G: Functor C D
(idtoiso (D -> E) T : morphism (D -> E) F F') oR G =
(idtoiso (C -> E) (ap (fun H0 : Functor D E => (H0 o G)%functor) T)
 :
 morphism (C -> E) (F o G)%functor (F' o G)%functor)
    path_natural_transformation; path_induction; simpl; auto with functor.
  Defined.
End composition.
Arguments isisomorphism_compose {H C D F' F''} T' {F} T {H0 H1}.
Arguments iso_whisker_l {H} C D E F G G' T {H0}.
Arguments iso_whisker_r {H} C D E F F' T G {H0}.

(** ** Equalities induced by isomorphisms of objects *)
Section object_isomorphisms.
  Lemma path_components_of_isisomorphism
        `{IsIsomorphism C s d m}
        D (F G : Functor C D) (T : NaturalTransformation F G)
  : (G _1 m)^-1 o (T d o F _1 m) = T s.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
(G _1 m)^-1 o (T d o F _1 m) = T s
  Proof.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
(G _1 m)^-1 o (T d o F _1 m) = T s
    apply iso_moveR_Vp.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
T d o F _1 m = G _1 m o T s
    apply commutes.
  Qed.

  Lemma path_components_of_isisomorphism'
        `{IsIsomorphism C s d m}
        D (F G : Functor C D) (T : NaturalTransformation F G)
  : (G _1 m o T s) o (F _1 m)^-1 = T d.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
G _1 m o T s o (F _1 m)^-1 = T d
  Proof.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
G _1 m o T s o (F _1 m)^-1 = T d
    apply iso_moveR_pV.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
G _1 m o T s = T d o F _1 m
    symmetry.
C: PreCategory
s, d: C
m: morphism C s d
H: IsIsomorphism m
D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
T d o F _1 m = G _1 m o T s
    apply commutes.
  Qed.

  Definition path_components_of_isomorphic
             `(m : @Isomorphic C s d)
             D (F G : Functor C D) (T : NaturalTransformation F G)
  : (G _1 m)^-1 o (T d o F _1 m) = T s
    := @path_components_of_isisomorphism _ _ _ m m D F G T.

  Definition path_components_of_isomorphic'
             `(m : @Isomorphic C s d)
             D (F G : Functor C D) (T : NaturalTransformation F G)
  : (G _1 m o T s) o (F _1 m)^-1 = T d
    := @path_components_of_isisomorphism' _ _ _ m m D F G T.
End object_isomorphisms.