Definition type_id_weq_iso (A B : ob type_precat) : (A = B) ≃ (iso A B) := weqcomp (univalence _ _) (type_equiv_weq_iso A B).
Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.Type.Core. Require Import UniMath.CategoryTheory.Categories.Type.MonoEpiIso.