{A B C : AbGroup@{u}} : ab_biprod (ab_biprod A B) C $<~> ab_biprod (ab_biprod C B) A. 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.
Require Import Basics Types Truncations.Core. Require Import WildCat. Require Import HSet. Require Import AbelianGroup. Require Import Modalities.ReflectiveSubuniverse.