Definition post_cat {X} {x y z:X} {p:y = z} : x = y -> x = z. Proof. intros q. exact (pathscomp0 q p). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom.