Functor sig_mor_as_sig sig_mor' := Build_Functor sig_mor_as_sig sig_mor' (@pr1_type _ _) (fun _ _ => idmap) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
Require Import HoTT.Tactics Types.Forall Types.Sigma Basics.Trunc. Require Import Category.Core Functor.Core Category.Sigma.Core. Require Import Functor.Paths. Import Functor.Identity.FunctorIdentityNotations. Import Functor.Composition.Core.FunctorCompositionCoreNotations.