fact: Definition isstrict_indiscrete_category `{H : IsHSet X} : IsStrictCategory (indiscrete_category X) := H.
imports: Functor.Core Category.Strict Category.Univalent Category.Morphisms Types.Unit Trunc HoTT.Tactics Equivalences