Definition induced_precategory_incl {M : precategory} {X:Type} (j : X -> ob M) : induced_precategory M j ⟶ M. Proof. use make_functor. - use make_functor_data. + exact j. + intros a b f. exact f. - repeat split. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence.