fact: Definition omega : PreCategory := @Build_PreCategory nat leq leq_refl (fun x y z p q => leq_trans q p) (fun _ _ _ _ _ _ _ => path_ishprop _ _) (fun _ _ _ => path_ishprop _ _) (fun _ _ _ => path_ishprop _ _) _.
imports: Category.Subcategory.Full Category.Sigma.Univalent Category.Morphisms Category.Univalent Category.Strict HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core