`{Funext} {G : Group} (N : Subgroup G) : IsNormalSubgroup N <~> (forall x y, N x -> N (y * x * -y)). Proof. rapply equiv_iff_hprop. - intros is_normal x y. exact (isnormal_conjugate (Build_NormalSubgroup G N is_normal)). - intros is_normal'. by snrapply Build_IsNormalSubgroup'. Defined.
Require Import Basics Types HFiber WildCat.Core. Require Import Truncations.Core. Require Import Algebra.Groups.Group TruncType.