Definition composition_preserves_unit {C D E : category} {IC : C} {ID : D} {IE : E} {F : functor C D} {G : functor D E} (puF : preserves_unit IC ID F) (puG : preserves_unit ID IE G) : preserves_unit IC IE (functor_composite F G) := puG · (functor_on_morphisms (pr1 G) puF).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation.