fact: Record SectionOfFunctor := { section_of_functor_morphism :> Functor D C; section_of_functor_issect : R o section_of_functor_morphism = 1 }.
imports: Functor.Core NaturalTransformation.Core Category.Strict Functor.Identity NaturalTransformation.Identity NaturalTransformation.Paths NaturalTransformation.Composition.Core Functor.Paths HoTT.Basics HoTT.Types