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