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