Lemma Functor_eq {A B: category} {F G:[A,B]} (ob : ∏ a, F ◾ a = G ◾ a) (mor : ∏ a a' f, transportf (λ k, k --> G ◾ a') (ob a) (transportf (λ k, F ◾ a --> k) (ob a') (F ▭ f)) = G ▭ f) : F = G. Proof. apply (invmap (Functor_eq_weq F G)). exists ob. exact mor. 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.