Isomorphic_full_sig_T <~> Isomorphic s d := (issig_isomorphic oE equiv_functor_sigma_id issig_isisomorphism). Global Instance trunc_Isomorphic : IsHSet (Isomorphic s d). Proof. eapply istrunc_equiv_istrunc; [ exact issig_isomorphic | ]. typeclasses eauto. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.