proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.CategoryTheory.DisplayedCats.Codomain UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod UniMath.CategoryTheory.DisplayedCats.DisplayedFunctorEq UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Preservation UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Examples.StructuredCategories UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.DispCatTerminal UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.FibTerminal UniMath.Bicategories.ComprehensionCat.BicatOfCompCat.CompCat UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispAdjunctions UniMath.Bicategories.DisplayedBicats.DispInvertibles UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.Prod UniMath.Bicategories.DisplayedBicats.Examples.FullSub UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat UniMath.Bicategories.DisplayedBicats.Examples.DispBicatOfDispCats