(F : to_prop C) : to_set C := Build_Functor C set_cat (fun x => Build_HSet (F x)) (fun s d m => (F _1 m)%morphism) (fun s d d' m m' => composition_of F s d d' m m') (fun x => identity_of F x).
Require Import Category.Core Functor.Core SetCategory.Core. Require Import Basics.Trunc.