Definition arrow_category (C : category) : category. Proof. use make_category. - use make_precategory_one_assoc; [apply (arrow_precategory_data C)|]. unfold is_precategory_one_assoc. split; [split|]. + intros a b f. unfold arrow_precategory_data in *; cbn in *. apply subtypePath. * intro; apply homset_property. * apply pathsdirprod; apply id_left. + intros a b f. unfold arrow_precategory_data in *; cbn in *. apply subtypePath. * intro; apply homset_property. * apply pathsdirprod; apply id_right. + intros a b c d f g h. apply subtypePath; [intro; apply homset_property|]. apply pathsdirprod; apply assoc. - intros a b. apply isaset_total2. + apply isaset_dirprod; apply homset_property. + intro. apply hlevelntosn. apply homset_property. 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.