Definition section_nat_trans_id (F : section_disp) : section_nat_trans_disp F F. Proof. use tpair. - intro. exact (id_disp _). - simpl. intros x x' f. rewrite id_left_disp, id_right_disp. unfold transportb. rewrite transport_f_f. apply maponpaths_2. apply homset_property. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core.