Proposition isaprop_is_democratic_functor {C₁ C₂ : full_comp_cat} (D₁ : is_democratic C₁) (D₂ : is_democratic C₂) (F : full_comp_cat_functor C₁ C₂) : isaprop (is_democratic_functor D₁ D₂ F). Proof. use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. use impred ; intro. apply homset_property. } use funextsec ; intro Γ. use subtypePath. { intro. apply isaprop_is_z_iso_disp. } use (invmaponpathsweq (disp_functor_ff_weq _ (full_comp_cat_comprehension_fully_faithful C₂) _ _ _)). use subtypePath. { intro. apply homset_property. } pose (!(pr2 φ₁ Γ) @ pr2 φ₂ Γ) as p. unfold democratic_functor_laws_mor in p. use (cancel_z_iso _ _ (comp_cat_extend_over_iso (is_democratic_ty D₂ (F Γ)) (TerminalArrow [] (F [])) (comp_cat_functor_empty_context_is_z_iso F))). use (cancel_z_iso' (comp_cat_functor_extension F [] (is_democratic_ty D₁ Γ))). use (cancel_z_iso' (functor_on_z_iso F (is_democratic_iso D₁ Γ))). exact p. 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.