Library UniMath.Bicategories.DisplayedBicats.Examples.CategoriesWithStructure.Equalizers
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Core.Prelude.
Require Import UniMath.CategoryTheory.Limits.Equalizers.
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.
Local Open Scope cat.
Section CategoriesWithChosenEqualizersAndPreservationUpToEquality.
Definition disp_bicat_chosen_equalizers
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, Equalizers C).
- exact (λ C₁ C₂ BP₁ BP₂ F, preserves_chosen_equalizers_eq F BP₁ BP₂).
- exact (λ C T, identity_preserves_chosen_equalizers_eq T).
- exact (λ _ _ _ _ _ _ _ _ PF PG, composition_preserves_chosen_equalizers_eq PF PG).
- exact (λ C, Equalizers C).
- exact (λ C₁ C₂ BP₁ BP₂ F, preserves_chosen_equalizers_eq F BP₁ BP₂).
- exact (λ C T, identity_preserves_chosen_equalizers_eq T).
- exact (λ _ _ _ _ _ _ _ _ PF PG, composition_preserves_chosen_equalizers_eq PF PG).
Definition cat_with_chosen_equalizers
: bicat
:= total_bicat disp_bicat_chosen_equalizers.
Lemma disp_2cells_iscontr_chosen_equalizers
: disp_2cells_iscontr disp_bicat_chosen_equalizers.
Show proof.
End CategoriesWithChosenEqualizersAndPreservationUpToEquality.
Section CategoriesWithExistingEqualizersAndPreservationUpToIso.
Definition disp_bicat_have_equalizers
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, hasEqualizers (C := C)).
- exact (λ C₁ C₂ _ _ F, preserves_equalizer F).
- exact (λ C _, identity_preserves_equalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_equalizer HF HG).
- exact (λ C, hasEqualizers (C := C)).
- exact (λ C₁ C₂ _ _ F, preserves_equalizer F).
- exact (λ C _, identity_preserves_equalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_equalizer HF HG).
Definition cat_with_equalizers
: bicat
:= total_bicat disp_bicat_have_equalizers.
Lemma disp_2cells_iscontr_have_equalizers
: disp_2cells_iscontr disp_bicat_have_equalizers.
Show proof.
End CategoriesWithExistingEqualizersAndPreservationUpToIso.
Section CategoriesWithChosenEqualizersAndPreservationUpToIso.
Definition disp_bicat_equalizers
: disp_bicat bicat_of_cats.
Show proof.
use disp_subbicat.
- exact (λ C, Equalizers C).
- exact (λ C₁ C₂ _ _ F, preserves_equalizer F).
- exact (λ C _, identity_preserves_equalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_equalizer HF HG).
- exact (λ C, Equalizers C).
- exact (λ C₁ C₂ _ _ F, preserves_equalizer F).
- exact (λ C _, identity_preserves_equalizer _).
- exact (λ _ _ _ _ _ _ _ _ HF HG, composition_preserves_equalizer HF HG).
Lemma disp_2cells_iscontr_equalizers
: disp_2cells_iscontr disp_bicat_equalizers.
Show proof.
End CategoriesWithChosenEqualizersAndPreservationUpToIso.