fact: Definition isstrict_chain {n} : IsStrictCategory [n].
imports: Category.Subcategory.Full Category.Sigma.Univalent Category.Morphisms Category.Univalent Category.Strict HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core