(A : object C^op) := Eval simpl in Functor.
Require Import Category.Core Functor.Core SetCategory.Core Category.Dual. Import Category.Prod.CategoryProdNotations Functor.Prod.Core.FunctorProdCoreNotations. Require Import Basics.Trunc.