Definition section_disp_cat : category. Proof. use make_category. - use make_precategory. + use make_precategory_data. * use make_precategory_ob_mor. -- exact section_disp. -- exact section_nat_trans_disp. * exact section_nat_trans_id. * do 3 intro. exact section_nat_trans_comp. + use make_is_precategory_one_assoc. * do 2 intro. exact section_nat_trans_id_left. * do 2 intro. exact section_nat_trans_id_right. * do 4 intro. exact section_nat_trans_assoc. - exact isaset_section_nat_trans_disp. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core.