Library UniMath.CategoryTheory.Categories.PrecategoryOfCategories

Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.FunctorCategory.

Local Open Scope cat.

Definition category_precategory_ob_mor
  : precategory_ob_mor
  := make_precategory_ob_mor
    category
    functor.

Definition category_precategory_data
  : precategory_data
  := make_precategory_data
    category_precategory_ob_mor
    (λ _, functor_identity _)
    (λ C₁ C₂ C₃ F G , F ∙ G).

Lemma category_precategory_is_precategory
  : is_precategory category_precategory_data.
Show proof.

  use make_is_precategory_one_assoc;
    intros;
    apply (functor_eq _ _ (homset_property _));
    now use functor_data_eq.

Definition category_precategory
  : precategory
  := make_precategory
    category_precategory_data
    category_precategory_is_precategory.