c : (a * b) c = F c. Proof. pose proof (ap (fun F => object_of F c) H1). pose proof (ap (fun F => object_of F c) H2). simpl in *. path_induction. apply eta_prod. 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.