proposition: Proposition finlim_dfl_comp_cat_unit_laws : is_pstrans finlim_dfl_comp_cat_unit_data.
proof: Proof. refine (_ ,, _ ,, _). - refine (λ (C₁ C₂ : univ_cat_with_finlim) (F G : functor_finlim C₁ C₂) (τ : nat_trans_finlim F G), _). use nat_trans_finlim_eq. intro x ; cbn. rewrite id_right, id_left. apply idpath. - refine (λ (C : univ_cat_with_finlim), _). Opaque comp_psfunctor. use nat_trans_finlim_eq. Transparent comp_psfunctor. intro x ; cbn. rewrite !id_left. apply idpath. - refine (λ (C₁ C₂ C₃ : univ_cat_with_finlim) (F : functor_finlim C₁ C₂) (G : functor_finlim C₂ C₃), _). Opaque comp_psfunctor. use nat_trans_finlim_eq. Transparent comp_psfunctor. intro x ; cbn. rewrite !id_left, !id_right. exact (!(functor_id _ _)). Opaque comp_psfunctor. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.Preservation UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Examples.StructuredCategories UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.ComprehensionCat.BicatOfCompCat UniMath.Bicategories.ComprehensionCat.DFLCompCat UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat UniMath.Bicategories.ComprehensionCat.Biequivalence.DFLCompCatToFinLim