path groupoid, constructed as a category

Definition path_groupoid (X:UU) : isofhlevel 3 X -> category.