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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.CategoryTheory.SimplicialSets.