Definition θ_functor_identity : StrengthForSignature (functor_identity [C, D]). Proof. use tpair. + use tpair. * intro x. { use tpair. - intro y; simpl; apply identity. - abstract (now intros y y' f; rewrite id_left, id_right). } * abstract (now intros y y' f; apply nat_trans_eq_alt; intro z; simpl; rewrite id_left, id_right). + now split; intros x; intros; apply nat_trans_eq_alt; intro c; simpl; rewrite !id_left. 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.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.CategoryTheory.BicatOfCatsElementary. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.CategoryTheory.PointedFunctorsComposition.