(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. destruct x, y; simpl. intros; path_induction; reflexivity. Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Functor.Composition.Core. Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core. Require Import Category.Morphisms FunctorCategory.Core. Require Import Pseudofunctor.Core. Require Import NaturalTransformation.Composition.Laws. Require Import Trunc Types.Sigma. Require Import Basics.Tactics. Import Functor.Identity.FunctorIdentityNotations. Module Import LaxCommaCategoryParts.