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