proposition: Lemma U_reflects_isos (n m : Δ) ( f : n --> m ) : (is_z_isomorphism ((# U) f)) -> (is_z_isomorphism f).
proof: Proof. intro I. use tpair. { exact (is_z_isomorphism_mor I,, mon_iso_mon_inv I). } cbv beta. exact (fincard_inv_is_inverse_in_precat n m f I). Defined.
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