Proposition eq_is_democratic {C : full_comp_cat} {D₁ D₂ : is_democratic C} (p : ∏ (Γ : C), is_democratic_ty D₁ Γ = is_democratic_ty D₂ Γ) (q : ∏ (Γ : C), is_democratic_iso D₁ Γ · comp_cat_comp_mor (idtoiso_disp (idpath _) (p Γ)) = is_democratic_iso D₂ Γ) : D₁ = D₂. Proof. use funextsec ; intro Γ. use total2_paths_f. - exact (p Γ). - use subtypePath. { intro. apply isaprop_is_z_isomorphism. } unfold z_iso. rewrite pr1_transportf. rewrite transportf_dem. exact (q Γ). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.CompCatNotations.