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 _ _ helper)) | (exists (path_forall _ _ (fun _ => Functor.Prod.Universal.unique idpath idpath))) ]; exp_laws_t; unfold helper, compose_fst_prod, compose_snd_prod, Functor.Prod.Universal.unique, Functor.Prod.Universal.unique_helper; exp_laws_t. Qed.
Require Import Category.Core Functor.Core. Require Import Functor.Prod. Require Import Functor.Paths. Require Import Functor.Identity Functor.Composition.Core. Require Import ExponentialLaws.Law3.Functors. Require Import Types.Prod ExponentialLaws.Tactics.