Proposition full_comp_cat_fiber_nat_trans_ax {C₁ C₂ : full_comp_cat} (F : full_comp_cat_functor C₁ C₂) (x : C₁) : is_nat_trans (fiber_functor (comp_cat_comprehension C₁) x ∙ fiber_functor (disp_codomain_functor F) x) (fiber_functor (comp_cat_type_functor F) x ∙ fiber_functor (comp_cat_comprehension C₂) (F x)) (comp_cat_functor_comprehension F x). Proof. intros xx xx' f. use eq_mor_cod_fib. refine (comp_in_cod_fib _ _ @ _ @ !(comp_in_cod_fib _ _)). cbn -[fiber_functor]. etrans. { apply maponpaths_2. apply disp_codomain_fiber_functor_mor. } pose (disp_nat_trans_ax (comp_cat_functor_comprehension F) (f := identity x) (xx := xx') (xx' := xx) f) as p. refine (maponpaths (λ z, pr1 z) p @ _). refine (transportb_cod_disp _ _ _ @ _). cbn. apply maponpaths. refine (!_). apply comprehension_functor_mor_transportf. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.NaturalTransformations. Require Import UniMath.CategoryTheory.DisplayedCats.Equivalences. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.StructuredCategories. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.DispCatTerminal. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.FibTerminal. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.CompCat. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats.