fact: Definition sig_functor_obj_inv : Functor sig_obj sig_obj_as_sig := Build_Functor sig_obj sig_obj_as_sig (fun x => x) (fun _ _ m => exist _ m tt) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
imports: HoTT.Basics HoTT.Types Category.Core Functor.Core Category.Sigma.Core Functor.Paths