fact: Definition attempt_paths {x} (f g : attempt x) : ∏ (e_fun : ∏ y pyx, f y pyx = g y pyx), (∏ y pyx, attempt_comp f y pyx @ maponpaths (H y) (funextsec (λ z, funextsec (λ lzy, e_fun z (cons (idpath z) lzy pyx)))) = e_fun y pyx @ attempt_comp g y pyx) -> f = g.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Univalence