c : inverse C1 C2 D (functor C1 C2 D c) = c. Proof. path_functor. exists (path_forall _ _ (helper2_helper c)). abstract (unfold helper2_helper; exp_laws_t). Defined.
Require Import Category.Core Functor.Core. Require Import Functor.Paths. Require Import Functor.Identity Functor.Composition.Core. Require Import ExponentialLaws.Law4.Functors. Require Import ExponentialLaws.Tactics.