proposition: Lemma path_morphism 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)), 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) -> gh = g'h'.
proof: Proof. intros Hg Hh Hp. destruct gh, g'h'; simpl in *. destruct Hg, Hh, Hp. 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