proposition: Lemma mon_iso_mon_inv {n m : Δ} {f : n --> m} (I : is_z_isomorphism ((# U) f)) : ∏ x y : (⟦m⟧)%stn, x ≤ y -> (is_z_isomorphism_mor I) x ≤ (is_z_isomorphism_mor I) y.
proof: Proof. intros x y l. unfold is_z_isomorphism in I. simpl in I. induction I as [I_fn I_is_inverse_in_preord], f as [f_fn f_guarantee]. induction (natlehchoice x y l) as [a | a']. - induction (natgthorleh (I_fn x) (I_fn y)). + contradiction (natlthtonegnatgeh x y a). assert (∏ z , f_fn (I_fn z) = z) as X. { intro z. change (f_fn (I_fn z)) with (compose (C:=Δ_sdg) I_fn f_fn z). simpl. set (j := (pr2 I_is_inverse_in_preord)). simpl in j. rewrite j. reflexivity. } rewrite <- (X x), <- (X y); apply f_guarantee. exact (natlthtoleh _ _ a0). + exact b. - simpl is_z_isomorphism_mor. apply subtypeInjectivity_prop in a'. induction a'. exact (isreflnatleh (I_fn x)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.NaturalNumbers UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.FiniteSets UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.CategoryTheory.SimplicialSets