(F G : Functor C (A * B)) (H1 : fst o F = fst o G) (H2 : snd o F = snd o G) : F = G. Proof. etransitivity; [ symmetry | ]; apply unique; try eassumption; reflexivity. Defined.
Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core. Require Import Functor.Paths. Require Import Types.Prod HoTT.Tactics Types.Forall Types.Sigma. Require Import Basics.Tactics.