functor' : Functor (0 * C) 0 := Functors.
Require Import HoTT.Basics HoTT.Types. Require Import Category.Core Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Prod Functor.Prod Functor.Composition.Core Functor.Identity Functor.Composition.Laws.