Definition hom_precat_data {C : two_cat} (x y : C) : precategory_data. Proof. use make_precategory_data. - exact (hom_precat_ob_mor x y). - exact (λ (f : x --> y), id2 f). - exact (λ (f g h : x --> y) (τ : f ==> g) (θ : g ==> h), τ • θ). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.Univalence.