proposition: Lemma path_morphism'_helper abf a'b'f' (gh g'h' : morphism abf a'b'f') : forall (Hg : gh.(g) = g'h'.(g)) (Hh : gh.(h) = g'h'.(h)), ((_ oL (Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ S _ _) Hg) : Category.Core.morphism _ _ _)) o (gh.(p)) o ((Category.Morphisms.idtoiso (_ -> _) (ap (@p_morphism_of _ _ T _ _) Hh) : Category.Core.morphism _ _ _)^-1 oR _) = g'h'.(p))%natural_transformation -> match Hg in _ = g, Hh in _ = h return NaturalTransformation (p_morphism_of T h o abf.(f)) (a'b'f'.(f) o p_morphism_of S g) with | idpath, idpath => gh.(p) end = g'h'.(p).
proof: Proof. simpl; intros Hg Hh Hp. destruct g'h'; simpl in *. destruct Hg, Hh, Hp; simpl in *. path_natural_transformation. autorewrite with functor morphism. reflexivity. Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Functor.Composition.Core NaturalTransformation.Paths NaturalTransformation.Composition.Core Category.Morphisms FunctorCategory.Core Pseudofunctor.Core NaturalTransformation.Composition.Laws Trunc Types.Sigma Basics.Tactics