Lemma type_id_weq_iso_is (A B : ob type_precat): @idtoiso _ A B = pr1 (type_id_weq_iso A B). Proof. apply funextfun. intro p; elim p. apply eq_iso; simpl. - apply funextfun; intro. apply idpath. Defined.
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.