proposition: Lemma is1natural_equiv_bg_pi1_adjoint_r `{Univalence} (X : pType) `{IsConnected 0 X} : Is1Natural (opyon (Pi1 X)) (opyon X o B) (equiv_bg_pi1_adjoint X).
proof: Proof. rapply (is1natural_natequiv (natequiv_bg_pi1_adjoint X)). Opaque equiv_bg_pi1_adjoint. Defined.
imports: Basics Types Pointed Cubical WildCat Algebra.AbGroups Homotopy.HSpace.Core TruncType Truncations.Core Truncations.Connectedness Homotopy.HomotopyGroup Homotopy.WhiteheadsPrinciple