Lemma isaprop_is_univalent (C : category) : isaprop (is_univalent C). Proof. apply impred. intro a. apply impred. intro b. apply isapropisweq. 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.