(** * Morphisms in a functor category *)
Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core.
Require Import Basics.Tactics.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope path_scope.
Local Open Scope category_scope.
Local Open Scope morphism_scope.

(** ** Natural Isomorphisms - isomorphisms in a functor category *)
Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G :=
  @Isomorphic (C -> D) F G.

Arguments NaturalIsomorphism {_} [C D] F G / .

Instance reflexive_natural_isomorphism `{Funext} C D
: Reflexive (@NaturalIsomorphism _ C D) | 0
  := _.

Coercion natural_transformation_of_natural_isomorphism `{Funext} C D F G
         (T : @NaturalIsomorphism _ C D F G)
: NaturalTransformation F G
  := T : morphism _ _ _.

Local Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.

(** ** If [T] is an isomorphism, then so is [T x] for any [x] *)
Definition isisomorphism_components_of `{Funext}
           `{@IsIsomorphism (C -> D) F G T} x
: IsIsomorphism (T x).
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
IsIsomorphism (T x)
Proof.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
IsIsomorphism (T x)
  exists (T^-1 x).
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
T^-1 x o T x = 1
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
T x o T^-1 x = 1
  -
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
T^-1 x o T x = 1 exact (apD10 (ap components_of left_inverse) x).
  -
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: morphism (C -> D) F G
H0: IsIsomorphism T
x: C
T x o T^-1 x = 1 exact (apD10 (ap components_of right_inverse) x).
Defined.

#[export]
Hint Immediate isisomorphism_components_of : typeclass_instances.
(** When one of the functors is the identity functor, we fail to match correctly, because [apply] is stupid.  So we do its work for it. *)
#[export]
Hint Extern 10 (@IsIsomorphism _ _ _ (@components_of ?C ?D ?F ?G ?T ?x))
=> apply (fun H' => @isisomorphism_components_of _ C D F G T H' x)
   : typeclass_instances.

Definition inverse
           C D (F G : Functor C D) (T : NaturalTransformation F G)
           `{forall x, IsIsomorphism (T x)}
: NaturalTransformation G F.
C, D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
H: forall x : C, IsIsomorphism (T x)
NaturalTransformation G F
Proof.
C, D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
H: forall x : C, IsIsomorphism (T x)
NaturalTransformation G F
  exists (fun x => (T x)^-1);
  abstract (
      intros;
      iso_move_inverse;
      first [ apply commutes
            | symmetry; apply commutes ]
    ).
Defined.

(** ** If [T x] is an isomorphism for all [x], then so is [T] *)
Definition isisomorphism_natural_transformation `{Funext}
           C D F G (T : NaturalTransformation F G)
           `{forall x, IsIsomorphism (T x)}
: @IsIsomorphism (C -> D) F G T.
H: Funext
C, D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
H0: forall x : C, IsIsomorphism (T x)
IsIsomorphism T
Proof.
H: Funext
C, D: PreCategory
F, G: Functor C D
T: NaturalTransformation F G
H0: forall x : C, IsIsomorphism (T x)
IsIsomorphism T
  exists (inverse _);
  abstract (
      path_natural_transformation;
      first [ apply left_inverse
            | apply right_inverse ]
    ).
Defined.

#[export]
Hint Immediate isisomorphism_natural_transformation : typeclass_instances.

(** ** Variant of [idtoiso] for natural transformations *)
Section idtoiso.
  Context `{Funext}.
  Variables C D : PreCategory.

  Definition idtoiso_natural_transformation
             (F G : object (C -> D))
             (T : F = G)
  : NaturalTransformation F G.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
NaturalTransformation F G
  Proof.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
NaturalTransformation F G
    refine (Build_NaturalTransformation'
              F G
              (fun x => idtoiso _ (ap10 (ap object_of T) x))
              _
              _);
    intros; case T; simpl;
    [ exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^)
    | exact (right_identity _ _ _ _ @ (left_identity _ _ _ _)^) ].
  Defined.

  Definition idtoiso
             (F G : object (C -> D))
             (T : F = G)
  : F <~=~> G.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
F <~=~> G
  Proof.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
F <~=~> G
    exists (idtoiso_natural_transformation T).
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
IsIsomorphism (idtoiso_natural_transformation T)
    exists (idtoiso_natural_transformation (T^)%path);
      abstract (path_natural_transformation; case T; simpl; auto with morphism).
  Defined.

  Lemma eta_idtoiso
        (F G : object (C -> D))
        (T : F = G)
  : Category.Morphisms.idtoiso _ T = idtoiso T.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
Morphisms.idtoiso (C -> D) T = idtoiso T
  Proof.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
Morphisms.idtoiso (C -> D) T = idtoiso T
    case T.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
Morphisms.idtoiso (C -> D) 1 = idtoiso 1
    expand; f_ap.
H: Funext
C, D: PreCategory
F, G: (C -> D)%category
T: F = G
isisomorphism_identity (C -> D) F =
{|
  morphism_inverse := idtoiso_natural_transformation 1;
  left_inverse := idtoiso_subproof F F 1%path;
  right_inverse := idtoiso_subproof0 F F 1%path
|}
    exact (center _).
  Qed.
End idtoiso.

Module Export FunctorCategoryMorphismsNotations.
  Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope.
End FunctorCategoryMorphismsNotations.