proposition: Lemma isweqpathsinv0 {X : Type} (x y : X) : isweq (@pathsinv0 X x y).
proof: Proof. intros. intros p. use tpair. - exists (!p). apply pathsinv0inv0. - cbn. intros [q k]. induction q,k. reflexivity. Defined.
imports: UniMath.Foundations.Preamble