proposition: Lemma Signature_category_Hstandard (H : [[C, D'], [C, D]]) (a a' : @StrengthForSignature C D D' H) : (∏ (X : [C, D']) (Y : category_Ptd C), Signature_category_mor_diagram (H,, a) (H,, a') (identity H) X Y) → (∏ (X : [C, D']) (Y : category_Ptd C), Signature_category_mor_diagram (H,, a') (H,, a) (identity H) X Y) → a = a'.
proof: Proof. intros leq geq. apply StrengthForSignature_eq. apply (nat_trans_eq (functor_category_has_homsets _ _ _)). intro XZ. assert (leqinst := leq (pr1 XZ) (pr2 XZ)). clear leq geq. red in leqinst. unfold theta in leqinst. etrans. { apply pathsinv0. apply id_right. } etrans. { exact leqinst. } clear leqinst. etrans. 2: { apply id_left. } apply cancel_postcomposition. apply nat_trans_eq; [apply homset_property |]. intro c. cbn. unfold horcomp_data; simpl. rewrite id_left. apply functor_id. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.FunctorCategory UniMath.SubstitutionSystems.Notation UniMath.SubstitutionSystems.Signatures UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.Core.Univalence UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.SumOfSignatures