Proposition is_disp_univalent_coalg_category {C : category} (F : C ⟶ C) : is_univalent_disp (coalgebra_disp_cat F). Proof. use is_univalent_disp_from_fibers. intros x f g. use isweqimplimpl. - intro p. pose (pr1 p) as q ; cbn in q. rewrite functor_id in q. rewrite id_left, id_right in q. exact q. - apply homset_property. - use isaproptotal2. + intro. apply isaprop_is_z_iso_disp. + intros. apply homset_property. 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.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.