Definition inv_algebra_mor_from_is_z_iso {X Y : FunctorAlg F} (f : X --> Y) : is_z_isomorphism (pr1 f) → (Y --> X). Proof. intro T. set (fiso:=make_z_iso' (pr1 f) T). set (finv:=inv_from_z_iso fiso). exists finv. unfold finv. apply pathsinv0. apply z_iso_inv_on_left. simpl. rewrite functor_on_inv_from_z_iso. rewrite <- assoc. apply pathsinv0. apply z_iso_inv_on_right. simpl. apply (pr2 f). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Arithmetic.NNO. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.Limits.Coproducts.