fact: Definition identity_of_helper_helper_object_of x : ap object_of (identity_of_helper_helper x) = idpath := path_functor_uncurried_fst _ _ _.
imports: Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths PathGroupoids Types.Forall HoTT.Tactics Basics.Tactics