proposition: Lemma helper1 c : functor C1 C2 D (inverse C1 C2 D c) = c.
proof: Proof. path_functor. abstract ( exp_laws_t; rewrite <- composition_of; exp_laws_t ). Defined.
imports: Category.Core Functor.Core Functor.Paths Functor.Identity Functor.Composition.Core ExponentialLaws.Law4.Functors ExponentialLaws.Tactics