proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.FullyFaithfulDispFunctor UniMath.CategoryTheory.Limits.Terminal UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.FullSub UniMath.Bicategories.ComprehensionCat.BicatOfCompCat UniMath.Bicategories.ComprehensionCat.CompCatNotations