Proposition all_functor_democratic_laws : democratic_functor_laws all_functor_democratic_data. Proof. intro Γ. refine (!_). unfold democratic_functor_laws_mor, all_functor_democratic_data. cbn -[comp_cat_functor_extension comp_cat_comp_z_iso comp_cat_extend_over_iso]. etrans. { do 2 apply maponpaths. apply maponpaths_2. apply (maponpaths pr1 (FF_disp_functor_ff_inv (full_comp_cat_comprehension_fully_faithful C₂) _)). } cbn -[comp_cat_extend_over_iso]. etrans. { apply maponpaths. rewrite !assoc. do 4 apply maponpaths_2. exact (z_iso_inv_after_z_iso (comp_cat_functor_extension F [] (is_democratic_ty D₁ Γ))). } rewrite id_left. rewrite !assoc. rewrite <- functor_comp. rewrite z_iso_inv_after_z_iso. rewrite functor_id. rewrite id_left. rewrite !assoc'. refine (_ @ id_right _). apply maponpaths. apply z_iso_after_z_iso_inv. 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.