proposition: Lemma Ff_point_unique {F : Ff C} (γ : Ff_lcomp_unit --> F) : γ = Ff_l_point F.
proof: Proof. apply subtypePath; [intro; apply isaprop_section_nat_trans_disp_axioms|]. use funextsec. intro f. use subtypePath; [intro; apply isapropdirprod; apply homset_property|]. set (test := three_mor_comm (section_nat_trans γ f)). use (pathscomp1 (pr1 (three_mor_comm (section_nat_trans γ f)))). - apply id_left. - apply id_left. 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 UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monoidal.CategoriesOfMonoids