Set-enriched categories #1467
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,160 @@ | ||
| Require Import UniMath.Foundations.PartA. | ||
| Require Import UniMath.Foundations.Sets. | ||
| Require Import UniMath.Foundations.Propositions. | ||
| Require Import UniMath.CategoryTheory.Core.Categories. | ||
| Require Import UniMath.CategoryTheory.Monoidal.MonoidalCategories. | ||
| Require Import UniMath.CategoryTheory.Enriched.Enriched. | ||
| Require Import UniMath.Bicategories.Core.Bicat. | ||
|
|
||
| Local Open Scope cat. | ||
|
|
||
| Section BicatOfEnrichedCat. | ||
|
|
||
| Definition enriched_precat_prebicat_data (Mon_V : monoidal_cat) : prebicat_data. | ||
| Proof. | ||
| use build_prebicat_data. | ||
| - exact (enriched_precat Mon_V). | ||
| - exact enriched_functor. | ||
| - exact (@enriched_nat_trans Mon_V). | ||
| - exact enriched_functor_identity. | ||
| - exact (@enriched_functor_comp Mon_V). | ||
| - exact (@enriched_nat_trans_identity Mon_V). | ||
| - exact (@enriched_nat_trans_comp Mon_V). | ||
| - exact (@pre_whisker Mon_V). | ||
| - exact (@post_whisker Mon_V). | ||
| - intros C D F. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, id_left; | ||
| reflexivity | ||
| ). | ||
|
Comment on lines
+29
to
+34
There was a problem hiding this comment. Here and elsewhere, the |
||
| - intros C D F. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, id_left; | ||
| reflexivity | ||
| ). | ||
| - intros C D F. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, id_right; | ||
| reflexivity | ||
| ). | ||
| - intros C D F. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, !id_right; | ||
| reflexivity | ||
| ). | ||
| - intros A B C D F G H. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, assoc; | ||
| reflexivity | ||
| ). | ||
| - intros A B C D F G H. | ||
| use make_enriched_nat_trans. | ||
| + intro x. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite postcompose_identity, precompose_identity, !assoc; | ||
| reflexivity | ||
| ). | ||
| Defined. | ||
|
|
||
| Lemma enriched_precat_prebicat_laws (Mon_V : monoidal_cat) : prebicat_laws (enriched_precat_prebicat_data Mon_V). | ||
| Proof. | ||
| repeat split; intros; use enriched_nat_trans_eq; intro; cbn. | ||
| - rewrite underlying_morphism_compose_swap, precompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_underlying_morphism_composite. | ||
| apply assoc. | ||
| - reflexivity. | ||
| - apply enriched_functor_on_identity. | ||
| - reflexivity. | ||
| - rewrite !assoc'. | ||
| apply cancel_precomposition. | ||
| apply pathsinv0. | ||
| apply enriched_functor_on_postcompose. | ||
| - rewrite postcompose_identity. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| reflexivity. | ||
| - rewrite postcompose_identity. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| reflexivity. | ||
| - rewrite postcompose_identity. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| reflexivity. | ||
| - rewrite postcompose_identity. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| rewrite assoc. | ||
| reflexivity. | ||
| - apply pathsinv0. | ||
| rewrite underlying_morphism_compose_swap. | ||
| rewrite !assoc'. | ||
| apply cancel_precomposition. | ||
| apply pathsinv0. | ||
| apply (enriched_nat_trans_ax y). | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite postcompose_identity. | ||
| apply id_right. | ||
| - rewrite underlying_morphism_compose_swap. | ||
| rewrite precompose_identity. | ||
| rewrite id_right. | ||
| apply enriched_functor_on_identity. | ||
| - rewrite enriched_functor_on_identity. | ||
| rewrite postcompose_identity. | ||
| apply id_right. | ||
| Qed. | ||
|
|
||
| Definition enriched_precat_prebicat (Mon_V : monoidal_cat) : prebicat := (_,, enriched_precat_prebicat_laws Mon_V). | ||
|
|
||
| Definition enriched_precat_bicat (Mon_V : monoidal_cat) : bicat. | ||
| Proof. | ||
| exists (enriched_precat_prebicat Mon_V). | ||
| intros C D F G. | ||
| apply isaset_enriched_nat_trans. | ||
| Defined. | ||
|
|
||
| End BicatOfEnrichedCat. | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,182 @@ | ||
| Require Import UniMath.Foundations.PartA. | ||
| Require Import UniMath.Foundations.Propositions. | ||
| Require Import UniMath.CategoryTheory.Core.Categories. | ||
| Require Import UniMath.CategoryTheory.Core.Functors. | ||
| Require Import UniMath.CategoryTheory.Monoidal.MonoidalCategories. | ||
| Require Import UniMath.CategoryTheory.Monoidal.MonoidalFunctors. | ||
| Require Import UniMath.CategoryTheory.Enriched.Enriched. | ||
| Require Import UniMath.CategoryTheory.Enriched.ChangeOfBase. | ||
| Require Import UniMath.Bicategories.Core.Bicat. | ||
| Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. | ||
| Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. | ||
| Require Import UniMath.Bicategories.EnrichedCategories.BicatOfEnrichedCat. | ||
|
|
||
| Local Open Scope cat. | ||
|
|
||
| Section PseudoFunctor. | ||
|
|
||
| Context {Mon_V Mon_V' : monoidal_cat} (F : lax_monoidal_functor Mon_V Mon_V'). | ||
|
|
||
| Definition change_of_base_psfunctor_data : psfunctor_data (enriched_precat_bicat Mon_V) (enriched_precat_bicat Mon_V'). | ||
| Proof. | ||
| use make_psfunctor_data. | ||
| - exact (change_of_base_enriched_precat F). | ||
| - exact (@change_of_base_enriched_functor _ _ F). | ||
| - exact (@change_of_base_enriched_nat_trans _ _ F). | ||
| - intro C. | ||
| use make_enriched_nat_trans. | ||
|
There was a problem hiding this comment. Here it would also be good to add separate definitions for the two natural transformations |
||
| + intro. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite (functor_id F), <- lax_monoidal_functor_on_postcompose_underlying_morphism, <- lax_monoidal_functor_on_precompose_underlying_morphism, postcompose_identity, precompose_identity; | ||
| reflexivity | ||
| ). | ||
| - intros. | ||
| use make_enriched_nat_trans. | ||
| + intro. | ||
| apply enriched_cat_id. | ||
| + intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite <- lax_monoidal_functor_on_postcompose_underlying_morphism, <- lax_monoidal_functor_on_precompose_underlying_morphism, postcompose_identity, precompose_identity, functor_comp; | ||
| reflexivity | ||
| ). | ||
| Defined. | ||
|
|
||
| Lemma change_of_base_psfunctor_laws : psfunctor_laws change_of_base_psfunctor_data. | ||
| Proof. | ||
| repeat split. | ||
| - intros C D G. | ||
| use enriched_nat_trans_eq. | ||
| intro. | ||
| reflexivity. | ||
| - intros a b f g h η φ. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite functor_comp. | ||
| rewrite lax_monoidal_functor_on_postcompose_underlying_morphism. | ||
| rewrite assoc. | ||
| reflexivity. | ||
| - intros a b f. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite <- lax_monoidal_functor_on_postcompose_underlying_morphism. | ||
| rewrite postcompose_identity. | ||
| rewrite functor_id. | ||
| rewrite !id_right. | ||
| rewrite assoc'. | ||
| rewrite <- functor_comp. | ||
| rewrite (enriched_functor_on_identity f). | ||
| reflexivity. | ||
| - intros a b f. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite <- lax_monoidal_functor_on_postcompose_underlying_morphism. | ||
| rewrite postcompose_identity. | ||
| rewrite functor_id. | ||
| rewrite !id_right. | ||
| reflexivity. | ||
| - intros a b c d f g h. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite (assoc' _ (#F _) (#F _)). | ||
| rewrite <- functor_comp. | ||
| rewrite (enriched_functor_on_identity h). | ||
| reflexivity. | ||
| - intros a b c f g₁ g₂ η. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism. | ||
| rewrite !assoc'. | ||
| apply cancel_precomposition. | ||
| rewrite <- !functor_comp. | ||
| apply maponpaths. | ||
| etrans. | ||
| { | ||
| apply underlying_morphism_compose_swap. | ||
| } | ||
| rewrite postcompose_identity, precompose_identity. | ||
| reflexivity. | ||
| - intros a b c f₁ f₂ g η. | ||
| use enriched_nat_trans_eq. | ||
| cbn. | ||
| intro x. | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism. | ||
| rewrite !assoc'. | ||
| apply cancel_precomposition. | ||
| rewrite <- !functor_comp. | ||
| apply maponpaths. | ||
| etrans. | ||
| { | ||
| apply underlying_morphism_compose_swap. | ||
| } | ||
| rewrite postcompose_identity, precompose_identity. | ||
| apply assoc'. | ||
| Qed. | ||
|
|
||
| Definition change_of_base_psfunctor : psfunctor (enriched_precat_bicat Mon_V) (enriched_precat_bicat Mon_V'). | ||
| Proof. | ||
| use make_psfunctor. | ||
| - exact change_of_base_psfunctor_data. | ||
| - exact change_of_base_psfunctor_laws. | ||
| - split. | ||
| + intros. | ||
| use make_is_invertible_2cell. | ||
|
There was a problem hiding this comment. For categories, one can prove that a natural transformation is an invertible 2-cell if it is a pointwise isomorphism. I guess the same holds in the enriched case. To improve the usability of your code, it would be good to add the notion of an isomorphism in an enriched category and to add the statement that a natural transformation is an invertible 2 -cell if and only if it is a pointwise isomorphism (this can be done in a separate PR though). |
||
| * use make_enriched_nat_trans. | ||
| -- intro x. | ||
| apply enriched_cat_id. | ||
| -- intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite functor_id, <- !lax_monoidal_functor_on_postcompose_underlying_morphism, <- lax_monoidal_functor_on_precompose_underlying_morphism, postcompose_identity, precompose_identity; | ||
| reflexivity | ||
| ). | ||
| * abstract ( | ||
| use enriched_nat_trans_eq; | ||
| intro x; | ||
| cbn; | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism, postcompose_identity, functor_id; | ||
| apply id_right | ||
| ). | ||
| * abstract ( | ||
| use enriched_nat_trans_eq; | ||
| intro x; | ||
| cbn; | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism, postcompose_identity, functor_id; | ||
| apply id_right | ||
| ). | ||
| + intros. | ||
| use make_is_invertible_2cell. | ||
| * use make_enriched_nat_trans. | ||
| -- intro x. | ||
| apply enriched_cat_id. | ||
| -- intros x y. | ||
| cbn. | ||
| abstract ( | ||
| rewrite functor_comp, <- !lax_monoidal_functor_on_postcompose_underlying_morphism, <- lax_monoidal_functor_on_precompose_underlying_morphism, postcompose_identity, precompose_identity; | ||
| reflexivity | ||
| ). | ||
| * abstract ( | ||
| use enriched_nat_trans_eq; | ||
| intro x; | ||
| cbn; | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism, postcompose_identity, functor_id; | ||
| apply id_right | ||
| ). | ||
| * abstract ( | ||
| use enriched_nat_trans_eq; | ||
| intro x; | ||
| cbn; | ||
| rewrite <- !lax_monoidal_functor_on_postcompose_underlying_morphism, postcompose_identity, functor_id; | ||
| apply id_right | ||
| ). | ||
| Defined. | ||
|
|
||
| End PseudoFunctor. | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it would be good to add a separate definition for this natural transformation and the next one.