`{Univalence} {A B : pType} `{IsConnected 0 A} `{IsConnected 0 B} (f : A ->* B) (e : IsEquiv (fmap loops f)) : IsEquiv f. Proof. apply isequiv_isbij_tr0_isequiv_loops. 1: apply isequiv_contr_contr. rapply conn_point_elim. srapply isequiv_homotopic'. - exact (equiv_concat_lr (point_eq f) (point_eq f)^ oE (Build_Equiv _ _ _ e)). - intro r. simpl. hott_simpl. Defined.
Require Import Basics Types. Require Import Pointed. Require Import WildCat.Core HFiber. Require Import Truncations. Require Import Algebra.Groups.Group. Require Import Homotopy.HomotopyGroup.