Library UniMath.CategoryTheory.Categories.Type.Univalence

Near-univalence of type_precat

The precategory of types is not quite univalent - it doesn't have hom-sets. However, it is the case that idtoiso is a weak equivalence.

Much of this material is copied near-verbatim from the results for sets.

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.

Local Open Scope cat.