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) _.
Require Import Functor.Core Category.Strict Category.Univalent Category.Morphisms. Require Import Types.Unit Trunc HoTT.Tactics Equivalences.