(fun x : Functor C D => 1 o x o 1) = idmap. Proof. apply path_forall; intro x. apply identity_of_helper_helper. Defined.
Require Import Category.Core Functor.Core Functor.Pointwise.Core NaturalTransformation.Core NaturalTransformation.Paths Functor.Composition.Core Functor.Identity Functor.Paths. Require Import PathGroupoids Types.Forall HoTT.Tactics. Require Import Basics.Tactics.