c x : inverse C1 C2 D (functor C1 C2 D c) x = c x. Proof. path_functor. abstract 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.