Definition has_equifiers_bicat_of_univ_cats : has_equifiers bicat_of_univ_cats. Proof. intros C₁ C₂ F G n₁ n₂. simple refine (_ ,, _ ,, _ ,, _). - exact (equifier_bicat_of_univ_cats n₁ n₂). - exact (equifier_bicat_of_univ_cats_pr1 n₁ n₂). - exact (equifier_bicat_of_univ_cats_eq n₁ n₂). - simple refine (_ ,, _ ,, _). + exact (equifier_bicat_of_univ_cats_ump_1 n₁ n₂). + exact (equifier_bicat_of_univ_cats_ump_2 n₁ n₂). + exact (equifier_bicat_of_univ_cats_ump_eq n₁ n₂). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Categories.Dialgebras. Require Import UniMath.CategoryTheory.Categories.CatIsoInserter. Require Import UniMath.CategoryTheory.Categories.EilenbergMoore. Require Import UniMath.CategoryTheory.Subcategory.Core. Require Import UniMath.CategoryTheory.Subcategory.Full. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.IsoCommaCategory. Require Import UniMath.CategoryTheory.CommaCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Examples.Reindexing. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Limits.Final. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.CommaObjects. Require Import UniMath.Bicategories.Limits.Inserters. Require Import UniMath.Bicategories.Limits.Equifiers. Require Import UniMath.Bicategories.Limits.IsoInserters. Require Import UniMath.Bicategories.Limits.EilenbergMooreObjects. Require Import UniMath.Bicategories.DisplayedBicats.Examples.MonadsLax. Require Import UniMath.Bicategories.Monads.Examples.MonadsInBicatOfUnivCats.