proposition: Lemma eisadj_path_natural_transformation : forall x, @eisretr_path_natural_transformation (path_inv x) = ap path_inv (eissect_path_natural_transformation x).
proof: Proof. repeat intro. refine (center _). Qed.
imports: Category.Core Functor.Core NaturalTransformation.Core Equivalences HoTT.Types Trunc Basics.Tactics