Definition Signature_category_displayed : disp_cat [[C,D'],[C,D]]. Proof. use disp_cat_from_SIP_data. - intro H. exact (@StrengthForSignature C D D' H). - intros H1 H2 str1 str2 α. exact (quantified_signature_category_mor_diagram (H1,,str1) (H2,,str2) α). - intros H1 H2 str1 str2 α. do 2 (apply impred; intro). apply functor_category_has_homsets. - intros H a X Z. apply SignatureMor_id_subproof. - intros H1 H2 H3 str1 str2 str3 a1 a2 a1mor a2mor. simpl in a1mor, a2mor. simpl. exact (SignatureMor_comp_subproof (H1,,str1) (H2,,str2) (H3,,str3) a1 a2 a1mor a2mor). Defined.
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.