proposition: Lemma ab_biprod_twist {A B C : AbGroup@{u}} : ab_biprod (ab_biprod A B) C $<~> ab_biprod (ab_biprod C B) A.
proof: Proof. snrapply Build_GroupIsomorphism. - snrapply Build_GroupHomomorphism. + intros [[a b] c]. exact ((c,b),a). + unfold IsSemiGroupPreserving. reflexivity. - snrapply isequiv_adjointify. + intros [[c b] a]. exact ((a,b),c). + reflexivity. + reflexivity. Defined.
imports: Basics Types Truncations.Core WildCat HSet AbelianGroup Modalities.ReflectiveSubuniverse