proposition: Proposition nat_trans_finlim_eq {C₁ C₂ : univ_cat_with_finlim} {F G : functor_finlim C₁ C₂} {τ₁ τ₂ : nat_trans_finlim F G} (p : ∏ (x : C₁), τ₁ x = τ₂ x) : τ₁ = τ₂.
proof: Proof. use subtypePath. { intro. use isapropdirprod ; use isapropdirprod ; exact isapropunit. } use nat_trans_eq. { apply homset_property. } exact p. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Preservation UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.DisplayedBicats.DispUnivalence UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell UniMath.Bicategories.DisplayedBicats.Examples.Prod