(c : Functor (C1 + C2) D) x : (1 o c o inl C1 C2 + 1 o c o inr C1 C2) x = c x. Proof. destruct x; reflexivity. Defined.
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.