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