Definition bicat_of_univ_cats_has_cores_coreflection : right_universal_arrow (groupoidal_to_inv2cells bicat_of_univ_cats). Proof. use make_right_universal_arrow'. - apply is_univalent_2_1_bicat_of_groupoidal. exact univalent_cat_is_univalent_2_1. - exact bicat_of_univ_cats_has_cores_map. - exact bicat_of_univ_cats_has_cores_counit. - intros C₀ C₀' F₁ F₂ α. simple refine ((_ ,, tt) ,, _). + exact (bicat_of_univ_cats_has_cores_nat_trans _ _ α). + abstract (use subtypePath ; [ intro ; apply isaprop_is_invertible_2cell | ] ; use nat_trans_eq ; [ apply homset_property | ] ; intro ; apply idpath). - abstract (intros C₀ C₀' F₁ F₂ α β₁ β₂ p q ; use subtypePath ; [ intro ; apply isapropunit | ] ; use nat_trans_eq ; [ apply homset_property | ] ; intro x ; use subtypePath ; [ intro ; apply isaprop_is_z_isomorphism | ] ; refine (nat_trans_eq_pointwise (maponpaths pr1 p) x @ !_) ; exact (nat_trans_eq_pointwise (maponpaths pr1 q) x)). - intros C₀ C₀' F. simple refine ((_ ,, tt) ,, _). + exact (@factor_through_core (pr11 C₀') (pr11 C₀ ,, groupoidal_obj_is_groupoid _ (pr2 C₀)) (pr1 F)). + cbn. use make_invertible_2cell. * simple refine (_ ,, _) ; cbn. ** exact (@factor_through_core_commute (pr11 C₀') (pr11 C₀ ,, groupoidal_obj_is_groupoid _ (pr2 C₀)) (pr1 F)). ** apply is_nat_z_iso_to_is_invertible_2cell. intro x. apply identity_is_z_iso. * apply is_invertible_2cell_bicat_of_inv2cells. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Elements. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.Core. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Projection. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.StreetOpFibration. Require Import UniMath.CategoryTheory.DisplayedCats.Examples. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayMapBicatSlice. Require Import UniMath.Bicategories.DisplayedBicats.Examples.BicatOfInvertibles. Require Import UniMath.Bicategories.Morphisms.FullyFaithful. Require Import UniMath.Bicategories.Morphisms.Eso. Require Import UniMath.Bicategories.Morphisms.InternalStreetOpFibration. Require Import UniMath.Bicategories.Morphisms.DiscreteMorphisms. Require Import UniMath.Bicategories.Morphisms.Examples.MorphismsInBicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Examples.FibrationsInBicatOfUnivCats. Require Import UniMath.Bicategories.Morphisms.Examples.EsosInBicatOfUnivCats. Require Import UniMath.Bicategories.Limits.Products. Require Import UniMath.Bicategories.Limits.Pullbacks. Require Import UniMath.Bicategories.Limits.PullbackFunctions. Require Import UniMath.Bicategories.Limits.Examples.BicatOfUnivCatsLimits. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.UniversalArrow. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Op2OfPseudoFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.OpFunctor. Require Import UniMath.Bicategories.PseudoFunctors.Examples.ConstProduct. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.Modifications.Modification. Require Import UniMath.Bicategories.OtherStructure.ClassifyingDiscreteOpfib. Require Import UniMath.Bicategories.OtherStructure.DualityInvolution. Require Import UniMath.Bicategories.OtherStructure.Exponentials. Require Import UniMath.Bicategories.OtherStructure.Cores.