fact: Definition to : Functor C (indiscrete_category X) := Build_Functor C (indiscrete_category X) objOf (fun _ _ _ => tt) (fun _ _ _ _ _ => idpath) (fun _ => idpath).
imports: Functor.Core Category.Strict Category.Univalent Category.Morphisms Types.Unit Trunc HoTT.Tactics Equivalences