Lemma Functor_eq_weq {A B: category} (F G:[A,B]) : F = G ≃ ∑ (ob : ∏ a, F ◾ a = G ◾ a), ∏ a a' f, transportf (λ k, k --> G ◾ a') (ob a) (transportf (λ k, F ◾ a --> k) (ob a') (F ▭ f)) = G ▭ f. Proof. exact (make_weq _ Functor_eq_map_isweq). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.RepresentableFunctors.Precategories. Require Import UniMath.MoreFoundations.Tactics.