proposition: Lemma law : functor D C1 C2 o inverse D C1 C2 = 1 /\ inverse D C1 C2 o functor D C1 C2 = 1.
proof: Proof. split; path_functor; [ (exists (path_forall _ _ helper1)) | (exists (path_forall _ _ helper2)) ]; exp_laws_t; unfold helper1, helper2; exp_laws_t. Qed.
imports: Functor.Core Category.Sum Functor.Sum Functor.Paths Functor.Identity Functor.Composition.Core Types.Prod ExponentialLaws.Tactics ExponentialLaws.Law2.Functors