Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.FiniteColimits
Bicategories for finite colimits
We define the bicategory of finitely cocomplete categories and finite colimit preserving functors.
In particular, we define the bicategories whose objects are categories equipped with colimits for a fixed diagram.
Contents.
1. Definition bicategories of categories equipped with
- an initial object disp_bicat_initial;
- binary coproducts disp_bicat_bincoproducts;
- and coequalizers respectively disp_bicat_coequalizers.
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Coequalizers.
Require Import UniMath.CategoryTheory.Limits.Preservation.
Require Import UniMath.CategoryTheory.DisplayedCats.Core.
Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations.
Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.
Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sub1Cell.
Require Import UniMath.Bicategories.DisplayedBicats.Examples.Prod.
Local Open Scope cat.
Section CategoriesWithChosenInitialAndPreservationUpToIso.
Definition disp_bicat_initial
: disp_bicat bicat_of_cats.
Show proof.
Lemma disp_2cells_iscontr_initial
: disp_2cells_iscontr disp_bicat_initial.
Show proof.
End CategoriesWithChosenInitialAndPreservationUpToIso.
Section CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
Definition disp_bicat_bincoproducts
: disp_bicat bicat_of_cats.
Show proof.
Lemma disp_2cells_iscontr_bincoproducts
: disp_2cells_iscontr disp_bicat_bincoproducts.
Show proof.
End CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
Section CategoriesWithChosenCoequalizersAndPreservationUpToIso.
Definition disp_bicat_coequalizers
: disp_bicat bicat_of_cats.
Show proof.
Lemma disp_2cells_iscontr_coequalizers
: disp_2cells_iscontr disp_bicat_coequalizers.
Show proof.
End CategoriesWithChosenCoequalizersAndPreservationUpToIso.
Definition disp_bicat_initial
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, Initial (C : category)).
- exact (λ C₁ C₂ _ _ F, preserves_initial F).
- exact (λ C _, identity_preserves_initial _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_initial HF HG).
- exact (λ C, Initial (C : category)).
- exact (λ C₁ C₂ _ _ F, preserves_initial F).
- exact (λ C _, identity_preserves_initial _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_initial HF HG).
Lemma disp_2cells_iscontr_initial
: disp_2cells_iscontr disp_bicat_initial.
Show proof.
End CategoriesWithChosenInitialAndPreservationUpToIso.
Section CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
Definition disp_bicat_bincoproducts
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, BinCoproducts C).
- exact (λ C₁ C₂ _ _ F, preserves_bincoproduct F).
- exact (λ C _, identity_preserves_bincoproduct _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_bincoproduct HF HG).
- exact (λ C, BinCoproducts C).
- exact (λ C₁ C₂ _ _ F, preserves_bincoproduct F).
- exact (λ C _, identity_preserves_bincoproduct _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_bincoproduct HF HG).
Lemma disp_2cells_iscontr_bincoproducts
: disp_2cells_iscontr disp_bicat_bincoproducts.
Show proof.
End CategoriesWithChosenBinCoproductsAndPreservationUpToIso.
Section CategoriesWithChosenCoequalizersAndPreservationUpToIso.
Definition disp_bicat_coequalizers
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, Coequalizers (C : category)).
- exact (λ C₁ C₂ _ _ F, preserves_coequalizer F).
- exact (λ C _, identity_preserves_coequalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_coequalizer HF HG).
- exact (λ C, Coequalizers (C : category)).
- exact (λ C₁ C₂ _ _ F, preserves_coequalizer F).
- exact (λ C _, identity_preserves_coequalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_coequalizer HF HG).
Lemma disp_2cells_iscontr_coequalizers
: disp_2cells_iscontr disp_bicat_coequalizers.
Show proof.
End CategoriesWithChosenCoequalizersAndPreservationUpToIso.
Section CategoriesWithChosenFiniteColimitsAndPreservationUpToIso.
Definition disp_bicat_colimits : disp_bicat bicat_of_cats
:= disp_dirprod_bicat
disp_bicat_initial
(disp_dirprod_bicat
disp_bicat_bincoproducts
disp_bicat_coequalizers).
Lemma disp_2cells_iscontr_colimits
: disp_2cells_iscontr disp_bicat_colimits.
Show proof.
End CategoriesWithChosenFiniteColimitsAndPreservationUpToIso.
Definition disp_bicat_colimits : disp_bicat bicat_of_cats
:= disp_dirprod_bicat
disp_bicat_initial
(disp_dirprod_bicat
disp_bicat_bincoproducts
disp_bicat_coequalizers).
Lemma disp_2cells_iscontr_colimits
: disp_2cells_iscontr disp_bicat_colimits.
Show proof.
End CategoriesWithChosenFiniteColimitsAndPreservationUpToIso.