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