Lemma isotoid_idtoiso (C : category) (H : is_univalent C) (a b : ob C) (p : a = b) : isotoid _ H (idtoiso p) = p. Proof. unfold isotoid. set (Hw := homotinvweqweq (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.