Lemma section_comp_nat_trans {F F' F'' : section_disp D} (nt : section_nat_trans_disp F F') (nt' : section_nat_trans_disp F' F'') : section_nat_trans (section_nat_trans_comp nt nt') = nat_trans_comp _ _ _ (section_nat_trans nt) (section_nat_trans nt'). Proof. apply nat_trans_eq_alt. intro c. use total2_paths_b. - exact (!id_left _). - apply (maponpaths (λ x, transportf _ x _)). exact (!pathsinv0inv0 _). Qed.
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.