proposition: Lemma Ff_iso_inv_LNWFS_mor (L L' : total_category (LNWFS C)) (iso : z_iso (pr1 L) (pr1 L')) (Hiso : (pr2 L) -->[iso] (pr2 L')) : pr2 L' -->[z_iso_inv iso] pr2 L.
proof: Proof. transparent assert (Hiso11 : (∏ f, is_z_isomorphism (three_mor11 (section_nat_trans (z_iso_mor iso) f)))). { intro f. exists (three_mor11 (section_nat_trans (z_iso_mor (z_iso_inv iso)) f)). split. - exact (eq_section_nat_trans_comp_component11 (pr122 iso) f). - exact (eq_section_nat_trans_comp_component11 (pr222 iso) f). } split; intro f. - use arrow_mor_eq. * etrans. apply id_left. etrans. exact (lnwfs_Σ_top_map_id (pr2 L) f). apply pathsinv0. etrans. apply cancel_postcomposition. apply cancel_postcomposition. exact (lnwfs_Σ_top_map_id (pr2 L') f). etrans. apply cancel_postcomposition. apply id_left. apply id_left. * set (inv := Hiso11 f). apply (pre_comp_with_z_iso_is_inj inv). etrans. apply assoc. etrans. apply cancel_postcomposition. exact (pr12 inv). etrans. apply id_left. etrans. exact (pathsinv0 (id_right _)). apply pathsinv0. etrans. apply assoc. etrans. apply cancel_postcomposition. etrans. apply assoc. apply cancel_postcomposition. exact (arrow_mor11_eq (pr1 Hiso f)). etrans. apply assoc'. etrans. apply assoc'. etrans. apply assoc'. apply cancel_precomposition. etrans. apply assoc. etrans. apply assoc. etrans. apply assoc4. etrans. apply cancel_postcomposition, cancel_precomposition. apply (LNWFS_comon_structure_whiskercommutes). etrans. apply cancel_postcomposition, assoc. etrans. apply assoc'. etrans. apply cancel_postcomposition. { etrans. apply (pr1_section_disp_on_morphisms_comp (pr1 L)). etrans. use (section_disp_on_eq_morphisms (pr1 L) (γ' := identity _)). - apply id_left. - exact (pr12 inv). - apply maponpaths. apply (section_disp_id (pr1 L)). } etrans. apply id_left. exact (eq_section_nat_trans_comp_component11 (pr122 iso) (fact_L (pr1 L) f)). - use arrow_mor_eq; [apply id_left|]. set (inv := Hiso11 f). apply (pre_comp_with_z_iso_is_inj inv). etrans. apply assoc. etrans. apply cancel_postcomposition. exact (pr12 inv). etrans. apply id_left. apply pathsinv0. exact (arrow_mor11_eq (pr2 Hiso f)). Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.EqDiag UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.Monads.Comonads UniMath.CategoryTheory.Monads.ComonadCoalgebras UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.NWFS UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Helpers UniMath.ModelCategories.Generated.MonoidalHelpers UniMath.ModelCategories.Generated.FFMonoidalStructure