{A B} {z z' : A + B} : path_sum_inv o (@path_sum _ _ z z') == idmap. Proof. intro p. destruct z, z', p; exact idpath. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.