Definition iscontr_attempt : ∏ x, iscontr (attempt x). Proof. apply (wwf_lt (λ x, iscontr_hProp (attempt x))). intros x IH. apply (iscontrretract _ _ assemble_disassemble). apply impred_iscontr; intro z; apply impred_iscontr; intro z'; apply impred_iscontr; intro l; apply impred_iscontr; intro e. induction e. exact (IH z l). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.