fact: Definition right_functor_nondep : Functor (sig_obj (C -> D) (fun F => { G : Functor D C & F -| G })) (sig_obj ((C -> D) * (D -> C)^op) (fun FG => fst FG -| snd FG)) := Build_Functor (sig_obj (C -> D) (fun F => { G : Functor D C & F -| G })) (sig_obj ((C -> D) * (D -> C)^op) (fun FG => fst FG -| snd FG)) (fun GFA => ((GFA.1, GFA.2.1); GFA.2.2)) (fun GFA G'F'A' m => (m, right_morphism_of_nondep G'F'A'.2.2 GFA.2.2 m)) (fun s d d' m1 m2 => path_prod' 1 (right_composition_of_nondep _ _ _ _ _)) (fun x => path_prod' 1 (right_identity_of_nondep _)).
imports: Category.Core Functor.Core Category.Dual FunctorCategory.Core Category.Sigma.OnObjects Category.Prod Adjoint.Core Adjoint.Functorial.Parts Adjoint.Functorial.Laws HoTT.Types.Prod