(F G : Functor C D) : path_functor'_T F G <~> (@equiv_inv _ _ _ equiv_sig_functor F = @equiv_inv _ _ _ equiv_sig_functor G). Proof. etransitivity; [ | by apply equiv_path_sigma ]. eapply @equiv_functor_sigma. repeat match goal with | [ |- context[(@equiv_inv ?A ?B ?f ?H ?F).1] ] => change ((@equiv_inv A B f H F).1) with (object_of F) end. Time exact (isequiv_idmap (object_of F = object_of G)). Abort. >> *)
Require Import Category.Core Functor.Core. Require Import HoTT.Basics HoTT.Types HoTT.Tactics.