Definition is_univalent_full_subcat (C : category) (univC : is_univalent C) (P : C → UU) : (∏ x : C, isaprop (P x)) → is_univalent (full_subcat C P). Proof. intro H. apply is_univalent_total_category. - exact univC. - exact (disp_full_sub_univalent _ _ H). Defined.
Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.