Lemma type_is_weq_idtoiso (A B : ob type_precat): isweq (@idtoiso _ A B). Proof. rewrite type_id_weq_iso_is. apply (pr2 (type_id_weq_iso A B)). 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.