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