fact: Definition issig_full_isomorphic : Isomorphic_full_sig_T <~> Isomorphic s d := (issig_isomorphic oE equiv_functor_sigma_id issig_isisomorphism).
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences