proposition: Lemma Law : functor C1 C2 D o inverse C1 C2 D = 1 /\ inverse C1 C2 D o functor C1 C2 D = 1.
proof: 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.
imports: Category.Core Functor.Core Functor.Prod Functor.Paths Functor.Identity Functor.Composition.Core ExponentialLaws.Law3.Functors Types.Prod ExponentialLaws.Tactics