(A B C : Type) : (A + B) + C <~> A + (B + C). Proof. simple refine (equiv_adjointify _ _ _ _). - intros [[a|b]|c]; [ exact (inl a) | exact (inr (inl b)) | exact (inr (inr c)) ]. - intros [a|[b|c]]; [ exact (inl (inl a)) | exact (inl (inr b)) | exact (inr c) ]. - intros [a|[b|c]]; reflexivity. - intros [[a|b]|c]; reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.