proposition: 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: Proof. apply (invmap (Functor_eq_weq F G)). exists ob. exact mor. Defined.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core