Definition path_comp_inv_inv {X} {a b c:X} (p:a = b) (q:b = c) : ! q @ ! p = ! (p @ q). Proof. intros. destruct p,q. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.