functor C1 C2 D o inverse C1 C2 D = 1 /\ inverse C1 C2 D o functor C1 C2 D = 1. Proof. split; path_functor; [ (exists (path_forall _ _ helper1)) | (exists (path_forall _ _ helper2)) ]; unfold helper1, helper2, helper2_helper; exp_laws_t. Qed.
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.