Lemma is_univalent_full_sub_category (H : is_univalent C) : is_univalent (full_sub_category C C'). Proof. unfold is_univalent. intros; apply isweq_sub_precat_paths_to_iso; assumption. Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Subcategory.Core.