Definition arrow_precategory_data (C : precategory) : precategory_data. Proof. use make_precategory_data. - use make_precategory_ob_mor. + exact (∑ (a : ob C × ob C), dirprod_pr1 a --> dirprod_pr2 a). + intros x y. exact (∑ fg : dirprod_pr1 (pr1 x) --> dirprod_pr1 (pr1 y) × dirprod_pr2 (pr1 x) --> dirprod_pr2 (pr1 y), pr2 x · dirprod_pr2 fg = dirprod_pr1 fg · pr2 y). - intros x; cbn. exists (make_dirprod (identity _) (identity _)). exact (id_right _ @ !id_left _). - intros x y z f g; cbn in *. exists (make_dirprod (dirprod_pr1 (pr1 f) · dirprod_pr1 (pr1 g)) (dirprod_pr2 (pr1 f) · dirprod_pr2 (pr1 g))). cbn. refine (assoc _ _ _ @ _). refine (maponpaths (fun x => x · _) (pr2 f) @ _). refine (_ @ assoc _ _ _). refine (_ @ maponpaths _ (pr2 g)). apply pathsinv0. apply assoc. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.Adjunctions.Core.