s d (m : morphism D s d) : NaturalTransformation !s !d. Proof. exists (fun _ : Unit => m); simpl; intros; clear; abstract (autorewrite with category; reflexivity). Defined.
Require Import Category.Core Functor.Core NaturalTransformation.Core. Require Import Category.Dual. Require Import Category.Prod. Require Import NaturalTransformation.Identity. Require Import FunctorCategory.Core Cat.Core. Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors. Import Comma.Core. Require Import HoTT.Tactics. Require Import Basics.Tactics.