proposition: Lemma LNWFS_tot_mor_eq {L L' : total_category (LNWFS C)} (τ τ' : L --> L') : (∏ (f : arrow C), pr1 (pr11 τ f) = pr1 (pr11 τ' f)) -> τ = τ'.
proof: Proof. intro H. apply subtypePath; [intro; apply isaprop_lnwfs_mor_axioms|]. apply subtypePath; [intro; apply isaprop_section_nat_trans_disp_axioms|]. apply funextsec. intro f. apply subtypePath; [intro; apply isapropdirprod; apply homset_property|]. exact (H f). 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.Monads.Monads UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.Lifting UniMath.ModelCategories.NWFS UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.LNWFSHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure