Definition section_nat_trans_comp {F F' F'': section_disp} (FF' : section_nat_trans_disp F F') (F'F'' : section_nat_trans_disp F' F'') : section_nat_trans_disp F F''. Proof. use tpair. - intro x. exact (transportf _ (id_left _) (FF' x ;; F'F'' x)). - simpl. intros x x' f. rewrite mor_disp_transportf_prewhisker. rewrite mor_disp_transportf_postwhisker. rewrite transport_f_f. rewrite assoc_disp_var, transport_f_f. rewrite <- (section_nt_disp_axioms_from_section_nt_disp F'F''). rewrite mor_disp_transportf_prewhisker, transport_f_f. do 2 rewrite assoc_disp, transport_f_b. rewrite <- (section_nt_disp_axioms_from_section_nt_disp FF'). rewrite mor_disp_transportf_postwhisker, 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.