proposition: Lemma locator'_locator_locator' (l' : locator' x) : locator_locator' (locator'_locator l') = l'.
proof: 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.
imports: HoTT.Basics HoTT.DProp HoTT.BoundedSearch HoTT.Spaces.Finite.Fin HoTT.ExcludedMiddle HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.cauchy HoTT.Classes.interfaces.archimedean HoTT.Classes.interfaces.round HoTT.Classes.interfaces.naturals HoTT.Classes.implementations.peano_naturals HoTT.Classes.orders.archimedean HoTT.Classes.orders.dec_fields HoTT.Classes.orders.lattices HoTT.Classes.theory.apartness HoTT.Classes.theory.rationals HoTT.Classes.orders.fields HoTT.Classes.theory.fields HoTT.Classes.theory.dec_fields