fact: Definition nat_trans_functor_id_right_inv (F : functor A B) : nat_trans F (functor_composite F (functor_identity B)) := nat_trans_functor_id_right F.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence