`{H : IsHSet X} : IsStrictCategory (indiscrete_category X) := H. Global Instance iscategory_indiscrete_category `{H : IsHProp X} : IsCategory (indiscrete_category X). Proof. intros. eapply (isequiv_adjointify (idtoiso (indiscrete_category X) (x := s) (y := d)) (fun _ => center _)); abstract ( repeat intro; destruct_head_hnf @Isomorphic; destruct_head_hnf @IsIsomorphism; destruct_head_hnf @Unit; path_induction_hammer ). Defined.
Require Import Functor.Core Category.Strict Category.Univalent Category.Morphisms. Require Import Types.Unit Trunc HoTT.Tactics Equivalences.