proposition: Lemma isaprop_preservesunit_commutes {C D : category} {IC : C} {ID : D} {F G : functor C D} (puF : preserves_unit IC ID F) (puG : preserves_unit IC ID G) (α : nat_trans F G) : isaprop (preservesunit_commutes puF puG α).
proof: Proof. apply homset_property. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos