proposition: Lemma eisretr_path_natural_transformation : path_inv o path_natural_transformation == idmap.
proof: Proof. repeat intro. refine (center _). Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Equivalences HoTT.Types Trunc Basics.Tactics