Proposition isaprop_is_regular_category (C : univalent_category) : isaprop (is_regular_category C). Proof. repeat (use isapropdirprod). - apply isaprop_Terminal. apply univalent_category_is_univalent. - apply isaprop_Pullbacks. apply univalent_category_is_univalent. - apply isaprop_coeqs_of_kernel_pair. - apply isaprop_regular_epi_pb_stable. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi.