Definition assemble_disassemble {x} (f : attempt x) : assemble_attempt (disassemble_attempt f) = f. Proof. use attempt_paths. - intros y [[|n] pyx]. + apply pathsinv0. use attempt_comp. + reflexivity. - intros y [[|n] pyx]. + cbn. refine (@maponpaths _ _ _ _ (idpath _) _ @ ! pathsinv0l _). refine (maponpaths _ _ @ funextsec_toforallpaths _). apply funextsec; intros z. apply (funextsec_toforallpaths (idpath _)). + refine (maponpaths _ _ @ pathscomp0rid _). refine (@maponpaths _ _ _ _ (idpath _) _). refine (maponpaths funextsec _ @ funextsec_toforallpaths _). apply funextsec; intros w. apply (funextsec_toforallpaths (idpath _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Univalence.