# Arrow categories

## Contents

• Definition
• As a comma category

## Definition

Section Defn.
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.
The commutative square pr1 x ---> pr1 y | | | | pr1 pr2 x ---> pr1 pr2 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.
(make_dirprod (identity _) (identity _)).
exact (id_right _ @ !id_left _).
- intros x y z f g; cbn in ×.
(make_dirprod (dirprod_pr1 (pr1 f) · dirprod_pr1 (pr1 g))
(dirprod_pr2 (pr1 f) · dirprod_pr2 (pr1 g))).
Composing commutative squares pr1 x ---> pr1 y ---> pr1 z | | | | f | g | | | | pr1 pr2 x ---> pr1 pr2 y ---> pr1 pr2 z
cbn.
refine (assoc _ _ _ @ _).
refine (maponpaths (fun xx · _) (pr2 f) @ _).
refine (_ @ assoc _ _ _).
refine (_ @ maponpaths _ (pr2 g)).
apply pathsinv0.
apply assoc.
Defined.

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.
End Defn.

## As a comma category

Definition arrow_category_eq_comma_category (C : category) :
comma_category (functor_identity C) (functor_identity C)
= arrow_category C.
Proof.
apply subtypePath.
- intro.
do 2 (apply impred; intro).
apply isapropisaset.
- use total2_paths_f.
+ cbn.
use total2_paths_f.
× reflexivity.
× apply pathsdirprod.
-- apply funextsec; intro.
use total2_paths_f; [reflexivity|].
apply proofirrelevance, homset_property.
-- do 5 (apply funextsec; intro).
use total2_paths_f; [reflexivity|].
apply proofirrelevance, homset_property.
+ apply proofirrelevance.
apply isaprop_is_precategory.
apply (pr2 (arrow_category C)).
Qed.