Definition section_disp_to_section : section_disp_cat D ⟶ [C, total_category D]. Proof. use make_functor. - use make_functor_data. + exact section_functor. + do 2 intro. exact section_nat_trans. - split. + exact section_id_nat_trans. + do 3 intro. exact section_comp_nat_trans. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing.