locator'_locator_locator' (l' : locator' x) : locator_locator' (locator'_locator l') = l'. Proof. enough (p : locsig ^-1 (locator_locator' (locator'_locator l')) = locsig ^-1 l'). - refine (equiv_inj (locsig ^-1) p). - unfold locsig; simpl. destruct l'; unfold locator'_locator, locator_locator'; simpl. apply path_sigma_hprop; simpl. apply path_forall; intro q; apply path_forall; intro r; apply path_arrow; intro nu. apply equiv_path_dhprop; simpl. rewrite (path_dec (locates_right0 q r nu)). destruct (dec (locates_right0 q r nu)); auto. Qed.
Require Import