Definition SignatureForgetfulFunctor : functor Signature_category [[C,D'],[C,D]]. Proof. use tpair. - use tpair. + intros F; apply (Signature_Functor F). + intros F G α; apply α. - abstract (now split). 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.