Lemma is_univalent_disp_from_fibers {C} {D : disp_cat C} : is_univalent_in_fibers D -> is_univalent_disp D. Proof. intros H x x' e. destruct e. apply H. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.