Functor cat cat := Build_Functor cat cat (fun C => (C.
Require Import Category.Core Functor.Core. Require Import Category.Dual Functor.Dual. Require Import Functor.Composition.Core Functor.Identity. Require Import Cat.Core Functor.Paths. Require Import Basics.Trunc Types.Sigma HoTT.Tactics Types.Forall.