proposition: Lemma Ff_lcomp_axioms (F' F : Ff C) : section_disp_axioms (Ff_lcomp_data F' F).
proof: Proof. split. - intro f. set (lf := fact_L F f). set (rf := fact_R F f). set (l'rf := fact_L F' rf). set (r'rf := fact_R F' rf). apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]. cbn. rewrite (section_disp_id F). etrans. use (section_disp_on_eq_morphisms' _ (γ := identity rf)). etrans. apply maponpaths. exact (section_disp_id F' rf). reflexivity. - intros f f' f'' γ γ'. apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]. apply pathsinv0. etrans. apply pr1_section_disp_on_morphisms_comp. use section_disp_on_eq_morphisms. * apply pr1_section_disp_on_morphisms_comp. * reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.Combinatorics.StandardFiniteSets UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers