proposition: Lemma path_object (x y : object) : forall (Ha : x.(a) = y.(a)) (Hb : x.(b) = y.(b)), match Ha in _ = X, Hb in _ = Y return Functor (S X) (T Y) with | idpath, idpath => x.(f) end = y.(f) -> x = y.
proof: Proof. destruct x, y; simpl. intros; path_induction; reflexivity. Defined.
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