Lemma constant_functor_composition_nat_trans (A B C : category) (b : B) (F : functor B C) : nat_trans (functor_composite (constant_functor A B b) F) (constant_functor A C (F b)). Proof. use make_nat_trans. + intro; apply identity. + abstract (intro; intros; apply maponpaths_2; exact (functor_id F b)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Chains.All.