{A B C D : Type} (F : A -> B) (G : C -> D) `{Is0Functor A B F, Is0Functor C D G} : Fun01 (A^op * C) (B^op * D). Proof. snrapply Build_Fun01. 1: exact (functor_prod F G). rapply is0functor_prod_functor. Defined.
Require Import Basics.Utf8 Basics.Overture Basics.Tactics Basics.Equivalences. Require Import WildCat.Core. Require Import WildCat.NatTrans. Require Import WildCat.Equiv. Require Import WildCat.Prod. Require Import WildCat.Opposite. Require Import WildCat.Yoneda. Require Import WildCat.FunctorCat. Require Import WildCat.Universe. Require Import Types.Prod.