fact: Definition indiscrete_category : PreCategory := @Build_PreCategory' X (fun _ _ => Unit) (fun _ => tt) (fun _ _ _ _ _ => tt) (fun _ _ _ _ _ _ _ => idpath) (fun _ _ _ _ _ _ _ => idpath) (fun _ _ f => match f with tt => idpath end) (fun _ _ f => match f with tt => idpath end) (fun _ => idpath) _.
imports: Functor.Core Category.Strict Category.Univalent Category.Morphisms Types.Unit Trunc HoTT.Tactics Equivalences