Lemma is_univalent_monics_cat (H : is_univalent C) : is_univalent subcategory_of_monics. Proof. intros a b. use weqhomot. - refine (iso_in_subcategory_of_monics_weq _ _ ∘ _)%weq. refine (make_weq _ (H _ _) ∘ _)%weq. refine (monics_subcategory_paths_weq _ _). - intro x. induction x. apply z_iso_eq. apply Monic_eq. reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.covyoneda. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Subcategory.Core.