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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.SIP. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures.