fact: Definition isequiv_is0connected_isequiv_loops `{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B} (f : A ->* B) (e : IsEquiv (fmap loops f)) : IsEquiv f.
imports: Basics Types Pointed WildCat.Core HFiber Truncations Algebra.Groups.Group Homotopy.HomotopyGroup