(** * Morphisms in cat *)
Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Core.
Require Import Category.Morphisms.

Set Implicit Arguments.
Generalizable All Variables.

Local Open Scope category_scope.
Local Open Scope morphism_scope.

(** ** Lemmas relationship between transporting the action of functors on objects, and [idtoiso] *)
Section iso_lemmas.
  Context `{Funext}.

  Variable C : PreCategory.

  Variables s d : C.
  Variables m1 m2 : morphism C s d.
  Variable p : m1 = m2.

  Variables Fs Fd : PreCategory.
  Variable Fm : morphism C s d -> Functor Fs Fd.

  Lemma transport_Fc_to_idtoiso
        s' d' u
  : @transport _ (fun m => morphism _ (Fm m s') d') _ _ p u
    = u o components_of (Category.Morphisms.idtoiso (_ -> _) (ap Fm p) : morphism _ _ _)^-1 s'.
H: Funext
C: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
Fs, Fd: PreCategory
Fm: morphism C s d -> Functor Fs Fd
s': Fs
d': Fd
u: morphism Fd ((Fm m1) _0 s')%object d'
transport (fun m : morphism C s d => morphism Fd ((Fm m) _0 s')%object d') p
  u =
u o (idtoiso (Fs -> Fd) (ap Fm p))^-1 s'
  Proof.
H: Funext
C: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
Fs, Fd: PreCategory
Fm: morphism C s d -> Functor Fs Fd
s': Fs
d': Fd
u: morphism Fd ((Fm m1) _0 s')%object d'
transport (fun m : morphism C s d => morphism Fd ((Fm m) _0 s')%object d') p
  u =
u o (idtoiso (Fs -> Fd) (ap Fm p))^-1 s'
    case p; clear p; simpl; autorewrite with morphism; reflexivity.
  Qed.

  Lemma transport_cF_to_idtoiso
        s' d' u
  : @transport _ (fun m => morphism _ s' (Fm m d')) _ _ p u
    = components_of (Category.Morphisms.idtoiso (_ -> _) (ap Fm p) : morphism _ _ _) d' o u.
H: Funext
C: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
Fs, Fd: PreCategory
Fm: morphism C s d -> Functor Fs Fd
s': Fd
d': Fs
u: morphism Fd s' ((Fm m1) _0 d')%object
transport (fun m : morphism C s d => morphism Fd s' ((Fm m) _0 d')%object) p
  u =
(idtoiso (Fs -> Fd) (ap Fm p) : morphism (Fs -> Fd) (Fm m1) (Fm m2)) d' o u
  Proof.
H: Funext
C: PreCategory
s, d: C
m1, m2: morphism C s d
p: m1 = m2
Fs, Fd: PreCategory
Fm: morphism C s d -> Functor Fs Fd
s': Fd
d': Fs
u: morphism Fd s' ((Fm m1) _0 d')%object
transport (fun m : morphism C s d => morphism Fd s' ((Fm m) _0 d')%object) p
  u =
(idtoiso (Fs -> Fd) (ap Fm p) : morphism (Fs -> Fd) (Fm m1) (Fm m2)) d' o u
    case p; clear p; simpl; autorewrite with morphism; reflexivity.
  Qed.
End iso_lemmas.