Definition cat_of_elems_data : precategory_data. Proof. exists cat_of_elems_ob_mor. split. + intros a. exists (identity (pr1 a)). abstract (exact (eqtohomot ((functor_id X) (pr1 a)) (pr2 a))). + intros a b c f g. exists (pr1 f · pr1 g). abstract (exact ((eqtohomot ((functor_comp X) (pr1 f) (pr1 g)) (pr2 a)) @ (maponpaths (# X (pr1 g)) (pr2 f) @ (pr2 g)))). 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.