path_natural_transformation o path_inv == idmap. Proof. repeat intro. refine (center _). Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.