Proposition full_comp_nat_trans_eq {C₁ C₂ : full_comp_cat} {F G : full_comp_cat_functor C₁ C₂} {τ₁ τ₂ : full_comp_cat_nat_trans F G} (p : ∏ (x : C₁), τ₁ x = τ₂ x) (p' := nat_trans_eq (homset_property _) _ _ _ _ p) (pp : ∏ (x : C₁) (xx : disp_cat_of_types C₁ x), transportf _ (nat_trans_eq_pointwise p' x) (comp_cat_type_nat_trans τ₁ x xx) = comp_cat_type_nat_trans τ₂ x xx) : τ₁ = τ₂. Proof. use subtypePath. { intro. use isapropdirprod ; apply isapropunit. } use subtypePath. { intro. apply isaprop_comprehension_nat_trans_eq. } use subtypePath. { intro. use isapropdirprod ; apply isapropunit. } use total2_paths_f. - use nat_trans_eq. { apply homset_property. } exact p. - etrans. { use transportf_dirprod. } use dirprodeq. + simpl. rewrite transportf_const. apply (proofirrelevance _ (isapropdirprod _ _ isapropunit isapropunit)). + simpl. use disp_nat_trans_eq. intros x xx. etrans. { use disp_nat_trans_transportf. } apply pp. 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.