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. 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.
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.