proposition: Lemma equiv_path_ideal `{Univalence} {R : CRing} {I J : Ideal R} : ideal_eq I J <~> I = J.
proof: Proof. refine ((equiv_ap' (issig_Ideal R)^-1 _ _)^-1 oE _). refine (equiv_path_sigma_hprop _ _ oE _). rapply equiv_path_subgroup'. Defined.
imports: Basics Types Spaces.Finite.Fin Classes.interfaces.abstract_algebra Algebra.Rings.CRing Algebra.AbGroups