proposition: Lemma eq_section_nat_trans_disp_on_morphism {C : category} {F F' : section_disp (three_disp C)} {γ γ' : section_nat_trans_disp F F'} : γ = γ' -> ∏ f, γ f = γ' f.
proof: Proof. intro H. now induction H. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three