{A B C} (f : C -> A + B) (z : decompose_r f) : is_inr (f (equiv_decompose f (inr z))) := z.2. Class Indecomposable (X : Type) := { indecompose : forall A B (f : X -> A + B), (forall x, is_inl (f x)) + (forall x, is_inr (f x)) ; indecompose0 : ~~X }. Global Instance indecomposable_contr `{Contr X} : Indecomposable X. Proof. constructor. - intros A B f. destruct (is_inl_or_is_inr (f (center X))); [ left | right ]; intros x. all:refine (transport _ (ap f (contr x)) _); assumption. - intros nx; exact (nx (center X)). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.