s d (m : morphism C s d) : G _1 m o CO s = CO d o F _1 m. Proof. case HM. case HO. exact (right_identity _ _ _ _ @ (left_identity _ _ _ _)^). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core.