Definition finlim_dfl_comp_cat_unit_data : pstrans_data (comp_psfunctor dfl_comp_cat_to_finlim_psfunctor finlim_to_dfl_comp_cat_psfunctor) (id_psfunctor bicat_of_univ_cat_with_finlim). Proof. use make_pstrans_data. - exact finlim_dfl_comp_cat_unit_mor. - exact (λ _ _ F, finlim_dfl_comp_cat_unit_natural_inv2cell F). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.Preservation. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Examples.StructuredCategories. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.ComprehensionCat.BicatOfCompCat. Require Import UniMath.Bicategories.ComprehensionCat.DFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.FinLimToDFLCompCat. Require Import UniMath.Bicategories.ComprehensionCat.Biequivalence.DFLCompCatToFinLim.