Definition loop_correspondence {T X Y} (f:T ≃ X) (g:T->Y) {t t':T} {l:t = t'} {m:f t = f t'} (mi:maponpaths f l = m) {n:g t = g t'} (ni:maponpaths g l = n) : maponpaths (funcomp (invmap f) g) m @ maponpaths g (homotinvweqweq f t') = maponpaths g (homotinvweqweq f t) @ 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.