forall x, @eisretr_path_natural_transformation (path_inv x) = ap path_inv (eissect_path_natural_transformation x). Proof. repeat intro. refine (center _). Qed.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Equivalences HoTT.Types Trunc Basics.Tactics.