fact: Definition pr1 : Functor category C := Build_Functor category C c (fun s d => @pr1 _ _) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
imports: Category.Core Functor.Core SetCategory.Core Basics.Trunc Types.Sigma Basics.Tactics