(** * Identity natural transformation *)
Require Import Category.Core Functor.Core NaturalTransformation.Core.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope morphism_scope.
Local Open Scope path_scope.
Local Open Scope natural_transformation_scope.

Section identity.
  Variables C D : PreCategory.

  (** There is an identity natural transformation.  We create a number
      of variants, for various uses. *)
  Section generalized.
    Variables F G : Functor C D.
    Hypothesis HO : object_of F = object_of G.
    Hypothesis HM : transport (fun GO => forall s d,
                                           morphism C s d
                                           -> morphism D (GO s) (GO d))
                              HO
                              (morphism_of F)
                    = morphism_of G.

    Local Notation CO c := (transport (fun GO => morphism D (F c) (GO c))
                                      HO
                                      (identity (F c))).

    Definition generalized_identity_commutes s d (m : morphism C s d)
    : CO d o F _1 m = G _1 m o CO s.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m =
G _1 m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism
    Proof.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m =
G _1 m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism
      case HM.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m =
transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) s d m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism case HO.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) 1 1%morphism
o F _1 m =
transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  1 (morphism_of F) s d m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) 1
    1%morphism
      exact (left_identity _ _ _ _ @ (right_identity _ _ _ _)^).
    Defined.

    Definition generalized_identity_commutes_sym s d (m : morphism C s d)
    : G _1 m o CO s = CO d o F _1 m.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
G _1 m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism =
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m
    Proof.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
G _1 m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism =
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m
      case HM.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) s d m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) HO
    1%morphism =
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) HO
  1%morphism
o F _1 m case HO.
C, D: PreCategory
F, G: Functor C D
HO: F = G
HM: transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  HO (morphism_of F) =
morphism_of G
s, d: C
m: morphism C s d
transport
  (fun GO : C -> D =>
   forall s0 d0 : C, morphism C s0 d0 -> morphism D (GO s0) (GO d0))
  1 (morphism_of F) s d m
o transport (fun GO : C -> D => morphism D (F _0 s)%object (GO s)) 1
    1%morphism =
transport (fun GO : C -> D => morphism D (F _0 d)%object (GO d)) 1 1%morphism
o F _1 m
      exact (right_identity _ _ _ _ @ (left_identity _ _ _ _)^).
    Defined.

    Definition generalized_identity
    : NaturalTransformation F G
      := Build_NaturalTransformation'
           F G
           (fun c => CO c)
           generalized_identity_commutes
           generalized_identity_commutes_sym.
  End generalized.

  Global Arguments generalized_identity_commutes / .
  Global Arguments generalized_identity_commutes_sym / .
  Global Arguments generalized_identity F G !HO !HM / .

  Section generalized'.
    Variables F G : Functor C D.
    Hypothesis H : F = G.

    Definition generalized_identity'
    : NaturalTransformation F G.
C, D: PreCategory
F, G: Functor C D
H: F = G
NaturalTransformation F G
    Proof.
C, D: PreCategory
F, G: Functor C D
H: F = G
NaturalTransformation F G
      apply (generalized_identity
               F G
               (ap (@object_of C D) H)).
C, D: PreCategory
F, G: Functor C D
H: F = G
transport
  (fun GO : C -> D =>
   forall s d : C, morphism C s d -> morphism D (GO s) (GO d))
  (ap object_of H) (morphism_of F) =
morphism_of G
      case H.
C, D: PreCategory
F, G: Functor C D
H: F = G
transport
  (fun GO : C -> D =>
   forall s d : C, morphism C s d -> morphism D (GO s) (GO d))
  (ap object_of 1) (morphism_of F) =
morphism_of F
      reflexivity.
    Defined.
  End generalized'.

  Definition identity (F : Functor C D)
  : NaturalTransformation F F
    := Eval simpl in @generalized_identity F F 1 1.

  Global Arguments generalized_identity' F G !H / .
End identity.

Global Arguments generalized_identity_commutes : simpl never.
Global Arguments generalized_identity_commutes_sym : simpl never.

Module Export NaturalTransformationIdentityNotations.
  Notation "1" := (identity _) : natural_transformation_scope.
End NaturalTransformationIdentityNotations.