Functor (S / T) ((T^op / S^op)^op) := Build_Functor (S / T) ((T^op / S^op)^op) (fun x => obj_of x) (fun s d m => mor_of s d m) (fun _ _ _ _ _ => 1%path) (fun _ => 1%path).
Require Import Category.Core Functor.Core. Require Import Category.Dual Functor.Dual. Require Import Functor.Composition.Core Functor.Identity. Import Comma.Core.