fact: Definition chain (n : nat) : PreCategory := { m : omega | m <= n }%category.
imports: Category.Subcategory.Full Category.Sigma.Univalent Category.Morphisms Category.Univalent Category.Strict HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core