Definition inv_arrow : y --> x. Proof. refine ((inv_from_z_iso (_,, Hf1) ,, inv_from_z_iso (_,, Hf2)) ,, _). abstract (cbn ; refine (!_) ; use z_iso_inv_on_left ; rewrite assoc' ; refine (!_) ; use z_iso_inv_on_right ; cbn ; exact (pr2 f)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.Adjunctions.Core.