Definition induced_precategory (M : precategory) {X:Type} (j : X -> ob M) : precategory. Proof. use tpair. - use tpair. + exact (X,, λ a b, precategory_morphisms (j a) (j b)). + split;cbn. * exact (λ c, identity (j c)). * exact (λ a b c, @compose M (j a) (j b) (j c)). - repeat split; cbn. + exact (λ a b, @id_left M (j a) (j b)). + exact (λ a b, @id_right M (j a) (j b)). + exact (λ a b c d, @assoc M (j a) (j b) (j c) (j d)). + exact (λ a b c d, @assoc' M (j a) (j b) (j c) (j d)). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos.