A B C (S : Functor A C) (T : Functor B C) : dual_functor S T o (dual_functor T^op S^op)^op = 1 /\ (dual_functor T^op S^op)^op o dual_functor S T = 1 := (idpath, idpath)%core.
Require Import Category.Core Functor.Core. Require Import Category.Dual Functor.Dual. Require Import Functor.Composition.Core Functor.Identity. Import Comma.Core.