Definition loop_correspondence' {X Y} {P:X->Type} (irr:∏ x (p q:P x), p = q) (sec:∏ x, P x) (g:total2 P->Y) {w w':total2 P} {l:w = w'} {m:weqpr1_irr_sec irr sec w = weqpr1_irr_sec irr sec w'} (mi:maponpaths (weqpr1_irr_sec irr sec) l = m) {n:g w = g w'} (ni:maponpaths g l = n) : maponpaths (funcomp (invmap (weqpr1_irr_sec irr sec)) g) m @ maponpaths g (homotinvweqweq' irr sec w') = maponpaths g (homotinvweqweq' irr sec w) @ n. Proof. intros. destruct ni, mi, l. simpl. rewrite pathscomp0rid. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.