proposition: Lemma fincard_inv_is_inverse_in_precat (n m : Δ) (f : n --> m ) (I : is_z_isomorphism ((# U) f)): is_inverse_in_precat f (is_z_isomorphism_mor I,, mon_iso_mon_inv I).
proof: Proof. unfold is_z_isomorphism in I. simpl in I. induction I as [g is_inverse], f as [ffun fguarantee]. simpl in is_inverse. induction is_inverse as [l r]. split. - apply morphism_extensionality. simpl. intro x. change ((@compose precat_fincard _ _ _ ffun g) x = x). simpl. rewrite l. reflexivity. - apply morphism_extensionality. intro x. simpl. change (ffun (g x)) with (compose (C:=Δ_sdg) g ffun x). simpl. rewrite r. unfold "id". reflexivity. 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