Lemma idtoiso_isotoid (C : category) (H : is_univalent C) (a b : ob C) (f : z_iso a b) : idtoiso (isotoid _ H f) = f. Proof. unfold isotoid. set (Hw := homotweqinvweq (make_weq idtoiso (H a b))). simpl in Hw. apply Hw. Qed.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos.