section_of_functor_sig' : section_of_functor_sig <~> SectionOfFunctor. Proof. issig. Defined.
Require Import Functor.Core NaturalTransformation.Core. Require Import Category.Strict. Require Import Functor.Identity NaturalTransformation.Identity. Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Core. Require Import Functor.Paths. Require Import HoTT.Basics HoTT.Types.