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