Set-enriched categories #1467

umedaikiti · 2022-03-06T03:51:57Z

This PR includes the following.

Monoidal structure on cartesian categories #1031 (auto and autorewrite are removed)
the bicategory of enriched categories
pseudofunctors between the bicategory of set-enriched categories and the bicategory of categories (without a proof that they constitute a biequivalence, which gives the valiadation suggested in Basic definitions and constructions for enriched category theory #1453)
the pseudofunctor that takes enriched categories and returns underlying categories

I believe that the proof of biequivalence is straightforward but I would like to finish it later because it requires a lot of efforts.

Univalence of slices

Street (op)fibrations in Cat

…ode, part 2

Duality involutions, rework discrete bicats

…to cartesian-monoidal

benediktahrens · 2022-03-06T18:00:22Z

The CI error comes from one of the "sanity" checks:

--- checking the ordering prescribed by the files UniMath/*/.packages/files ---
error: *** UniMath/CategoryTheory/Enriched/ChangeOfBase.vo should not require UniMath/CategoryTheory/Enriched/BicatOfEnrichedCat.vo
error: *** UniMath/CategoryTheory/Enriched/ChangeOfBase.vo should not require UniMath/Bicategories/Core/Bicat.vo
error: *** UniMath/CategoryTheory/Enriched/ChangeOfBase.vo should not require UniMath/Bicategories/PseudoFunctors/PseudoFunctor.vo
error: *** UniMath/CategoryTheory/Enriched/ChangeOfBase.vo should not require UniMath/Bicategories/PseudoFunctors/Display/PseudoFunctorBicat.vo
error: *** UniMath/CategoryTheory/Enriched/BicatOfEnrichedCat.vo should not require UniMath/Bicategories/Core/Bicat.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/Core/Bicat.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/PseudoFunctors/PseudoFunctor.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/PseudoFunctors/Display/PseudoFunctorBicat.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/Transformations/PseudoTransformation.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/Core/Examples/BicatOfCats.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/PseudoFunctors/Examples/Composition.vo
error: *** UniMath/CategoryTheory/Enriched/HSETEnriched.vo should not require UniMath/Bicategories/PseudoFunctors/Biequivalence.vo
12 dependency order errors in package listings
make: *** [Makefile:321: .check-prescribed-ordering.okay] Error 1

In general, the list of files in .package/files should be considered to be ordered by dependency. A file B importing file A should be listed after file A.
Here, this means that the file Enriched/HSETEnriched.v should be listed after the files mentioned in the message above.

umedaikiti · 2022-03-07T07:13:36Z

The sanity checks passed, but the build script failed with the message "Error: Universe inconsistency." I don't think I did anything strange. No error occurs when I run make in my local environment. Do you have any idea about the reason for this failure?

benediktahrens · 2022-03-07T09:09:11Z

The sanity checks passed, but the build script failed with the message "Error: Universe inconsistency." I don't think I did anything strange. No error occurs when I run make in my local environment. Do you have any idea about the reason for this failure?

There are two builds launched for each PR:

A build of UniMath itself, called "CI-Build-UniMath / Build-UniMath-and-Sanity-Checks".
A build of parts of UniMath, and a complete build of the satellite repositories, called "CI-Build-Satellites / build".

It is the second one that failed, specifically when building the satellite repository https://github.com/UniMath/SetHITs.

@nmvdw : could you assist in investigating this error?

benediktahrens · 2022-03-07T10:10:18Z

UniMath/Bicategories/EnrichedCategories/BicatOfEnrichedCat.v

+    + intros x y.
+      cbn.
+      abstract (
+        rewrite postcompose_identity, precompose_identity, id_left;
+        reflexivity
+      ).


Here and elsewhere, the abstract(...) could/should also include the intros.... cbn. tactics.

benediktahrens · 2022-03-07T10:13:55Z

UniMath/CategoryTheory/limits/products.v

+
+  (** The arrow from p1 to p2 induced by the projections from p1 is an iso *)
+  Lemma product_unique (p1 p2 : Product I C c) :
+    is_iso (ProductArrow _ _ p2 (ProductPr I C p1)).


We are transitioning to is_z_iso, so maybe it would be best to state this lemma directly in terms of it? The proof should be the same after is_iso_qinv.

benediktahrens · 2022-03-07T10:14:19Z

UniMath/CategoryTheory/limits/products.v

+        apply funextsec; intro.
+        rewrite ProductPrCommutes.
+        now rewrite id_left.
+  Qed.


This proof should be transparent, at least in part, to allow for the extraction of the inverse.

benediktahrens · 2022-03-07T10:14:35Z

UniMath/CategoryTheory/limits/products.v

+  unfold isProduct.
+  do 2 (apply impred; intro).
+  apply isapropiscontr.
+Defined.


Suggested change

Defined.

Qed.

benediktahrens · 2022-03-07T10:15:46Z

UniMath/CategoryTheory/limits/binproducts.v

+  Local Definition r_pr2 {x y z : C} : C ⟦x ⊠ (y ⊠ z), y⟧ := π2 · π1.
+  Local Definition r_pr3 {x y z : C} : C ⟦x ⊠ (y ⊠ z), z⟧ := π2 · π2.
+
+  Lemma right_assoc_ternary_product :


It might be good to make parts of this construction opaque.

benediktahrens · 2022-03-07T10:16:01Z

UniMath/CategoryTheory/limits/binproducts.v

+  Local Definition l_pr2 {x y z : C} : C ⟦(x ⊠ y) ⊠ z, y⟧ := π1 · π2.
+  Local Definition l_pr3 {x y z : C} : C ⟦(x ⊠ y) ⊠ z, z⟧ := π2.
+
+  Lemma left_assoc_ternary_product :


It might be good to make parts of this construction opaque.

benediktahrens · 2022-03-07T10:16:40Z

UniMath/CategoryTheory/limits/binproducts.v

+        isweq BinproductsToProductsBool.
+  Proof.
+    apply (isweq_iso _ ProductsBoolToBinproducts).
+    - intros x.


It might be good to make parts of this construction opaque.

benediktahrens · 2022-03-07T10:19:49Z

UniMath/CategoryTheory/limits/binproducts.v

@@ -696,6 +701,15 @@ Arguments isBinProduct' _ _ _ _ _ : clear implicits.

 (** ** Terminal object as the unit (up to isomorphism) of binary products *)

+(** Generalize [maponpaths_2] to this lemma *)
+Local Lemma f_equal_2 :


There are already two constructions for this:

two_arg_paths: ∏ (A B C : UU) (f : A → B → C) (a1 : A) (b1 : B) (a2 : A) (b2 : B), a1 = a2 → b1 = b2 → f a1 b1 = f a2 b2 map_on_two_paths: ∏ (X Y Z : UU) (f : X → Y → Z) (x x' : X) (y y' : Y), x = x' → y = y' → f x y = f x' y'

nmvdw · 2022-03-07T10:42:16Z

The sanity checks passed, but the build script failed with the message "Error: Universe inconsistency." I don't think I did anything strange. No error occurs when I run make in my local environment. Do you have any idea about the reason for this failure?

There are two builds launched for each PR:

A build of UniMath itself, called "CI-Build-UniMath / Build-UniMath-and-Sanity-Checks".

A build of parts of UniMath, and a complete build of the satellite repositories, called "CI-Build-Satellites / build".

It is the second one that failed, specifically when building the satellite repository https://github.com/UniMath/SetHITs.

@nmvdw : could you assist in investigating this error?

Interestingly, the error happens in the following line: Require Export UniMath.CategoryTheory.limits.binproducts.. The same error message is given if I replace it by Require Import UniMath.CategoryTheory.limits.binproducts..

The error can be avoided by adding -arg "-type-in-type" in the _CoqProject file.

My guess is that one of the additions to UniMath.CategoryTheory.limits.binproducts requires impredicativity of universes.

nmvdw

Some tips for constructing the biequivalence:

I think it is useful to have a separate statement for constructing invertible 2-cells (pointwise isos are invertible 2-cells). For a biequivalence, you need to construct numerous invertible 2-cells and you can save work by having a more efficient way for constructing invertible 2-cells.
Sometimes, I meet termination issues when constructing biequivalences (non-termination at the Qed or Defined). To deal with this, comp_psfunctor need to be made opaque at several parts (see for example https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/DualityInvolution.v or https://github.com/UniMath/UniMath/blob/master/UniMath/Bicategories/DisplayedBicats/FiberBicategory/TrivialFiber.v and especially the lines which contain Transparent comp_psfunctor or Opaque comp_psfunctor).

Another thing that I am wondering about, is how do you envision the role of univalence in your development and what are your plans in this regard? For both categories and bicategories, the main focus in univalent foundations tends to be on the univalent ones.

nmvdw · 2022-03-07T10:43:52Z

UniMath/Bicategories/EnrichedCategories/BicatOfEnrichedCat.v

+  - exact (@pre_whisker Mon_V).
+  - exact (@post_whisker Mon_V).
+  - intros C D F.
+    use make_enriched_nat_trans.


I think it would be good to add a separate definition for this natural transformation and the next one.

nmvdw · 2022-03-07T10:46:26Z

UniMath/Bicategories/EnrichedCategories/ChangeOfBase.v

+  - exact (@change_of_base_enriched_functor _ _ F).
+  - exact (@change_of_base_enriched_nat_trans _ _ F).
+  - intro C.
+    use make_enriched_nat_trans.


Here it would also be good to add separate definitions for the two natural transformations

nmvdw · 2022-03-07T10:48:58Z

UniMath/Bicategories/EnrichedCategories/ChangeOfBase.v

+  - exact change_of_base_psfunctor_laws.
+  - split.
+    + intros.
+      use make_is_invertible_2cell.


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).

nmvdw · 2022-03-07T10:50:27Z

UniMath/CategoryTheory/Enriched/HSETEnriched.v

+      exact (F x).
+    + intros x y f.
+      exact (enriched_functor_on_morphisms F _ _ f).
+  - split.


This should be made opaque.

nmvdw · 2022-03-07T10:50:44Z

UniMath/CategoryTheory/Enriched/HSETEnriched.v

+  use make_nat_trans.
+  - intro x.
+    exact (a x tt).
+  - intros x y f.


This should be made opaque.

nmvdw · 2022-03-07T10:52:49Z

UniMath/CategoryTheory/Monoidal/Cartesian.v

+        use make_is_z_isomorphism.
+        * apply binprod_assoc_r.
+        * apply assoc_l_qinv_assoc_r.
+    - intros a b; cbn.


The parts following this need to be made opaque.

m-lindgren

With these changes SetHITs should not have to enable -type-in-type.

I would prefer if there wasn't duplication of material, but since this PR has been around a while I don't mind, we can clean it up later.

I have no comments on the mathematics of this, I just looked at the SetHIT-problem.

UniMath/CategoryTheory/limits/binproducts.v

m-lindgren · 2022-11-06T22:03:24Z

UniMath/CategoryTheory/limits/binproducts.v

+  Let α {x y z} : C⟦(x ⊠ y) ⊠ z, x ⊠ (y ⊠ z)⟧ := binprod_assoc x y z.
+
+  (** A type with three inhabitants, used for indexing ternary products *)
+  Let three : UU := coprod unit bool.


There's already a type like this in Combinatorics/StandardFiniteSets.v

UniMath/CategoryTheory/limits/binproducts.v

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

m-lindgren · 2022-11-18T17:10:11Z

Can we try and merge master into this and see if it compiles with the recent changes to UniMath?

benediktahrens · 2022-11-18T17:20:38Z

Can we try and merge master into this and see if it compiles with the recent changes to UniMath?

Done!

UniMath/CategoryTheory/Monoidal/Cartesian.v

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

langston-barrett and others added 30 commits November 22, 2021 23:27

Uniqueness of general products (up to isomorphism)

d884132

Associativity of binary products

0d97d7f

Fix notation conflict

b222d1f

monoidal structure on categories with products

c13d72e

Migrate proof of binary product associativity to binproducts.v

e629c8b

Add Cartesian.v to CONTENTS.md

dabdc7b

fix errors

ca9bf06

Merge branch 'master' into univalence-slices

38574c7

Merge pull request UniMath#1457 from nmvdw/univalence-slices

2d319b9

Univalence of slices

Street (op)fibs in Cat

096421b

Merge branch 'master' into street-fib-in-cat

70324d3

Merge pull request UniMath#1458 from nmvdw/street-fib-in-cat

d2273bf

Street (op)fibrations in Cat

try to get the unicode notation table to look nice in ASCII viewing mode

d04c63d

Merge branch 'master' of github.com:UniMath/UniMath

36b3874

add some remarks about emacs to USAGE.md

5ff1ae2

try to get the unicode notation table to look nice in ASCII viewing m…

c725e07

…ode, part 2

Duality involutions, rework discrete bicats

f3bb66e

Merge branch 'master' into duality-involution

393e08c

Whoops....

fc49805

Remove comments

d239668

Forgot to add a file

368f71d

Merge pull request UniMath#1460 from nmvdw/duality-involution

91d2bb0

Duality involutions, rework discrete bicats

Uniqueness of general products (up to isomorphism)

6cc9f2e

Associativity of binary products

8018188

Fix notation conflict

e1dd9d7

monoidal structure on categories with products

6c4c07b

Migrate proof of binary product associativity to binproducts.v

7e7b846

Add Cartesian.v to CONTENTS.md

740c86e

fix errors

2eeccd0

remove obsolete file Cats.v with def of precat of cats

503a80e

umedaikiti and others added 6 commits March 4, 2022 22:30

Merge branch 'cartesian-monoidal' of github.com:umedaikiti/UniMath in…

6d7c516

…to cartesian-monoidal

add correspondence between HSET-enriched and ordinary categories

2ac52f4

improve proofs

126a7e9

Merge branch 'UniMath:master' into cartesian-monoidal

39ea615

Merge branch 'UniMath:master' into cartesian-monoidal

ea2e038

remove auto and autorewrite

0a08dae

move some parts to UniMath/Bicategories/EnrichedCategories

16ae6a5

benediktahrens requested a review from rmatthes March 7, 2022 09:05

benediktahrens mentioned this pull request Mar 7, 2022

Is flag -type-in-type required for this repository? UniMath/SetHITs#3

Closed

benediktahrens reviewed Mar 7, 2022

View reviewed changes

nmvdw approved these changes Mar 7, 2022

View reviewed changes

benediktahrens added 2 commits March 11, 2022 19:55

Merge branch 'master' into cartesian-monoidal

18f4a6c

Merge branch 'master' into cartesian-monoidal

7166753

m-lindgren requested changes Nov 6, 2022

View reviewed changes

benediktahrens and others added 6 commits November 7, 2022 10:11

Update UniMath/CategoryTheory/limits/binproducts.v

70c125f

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

Update UniMath/CategoryTheory/limits/binproducts.v

9788301

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

Update UniMath/CategoryTheory/limits/binproducts.v

2a7cdc5

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

Update UniMath/CategoryTheory/limits/binproducts.v

5d42579

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

Update UniMath/CategoryTheory/limits/binproducts.v

7c41460

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

Merge branch 'master' into cartesian-monoidal

98f0cc6

Merge branch 'master' into cartesian-monoidal

41339c6

m-lindgren reviewed Nov 18, 2022

View reviewed changes

UniMath/CategoryTheory/Monoidal/Cartesian.v Outdated Show resolved Hide resolved

Update UniMath/CategoryTheory/Monoidal/Cartesian.v

9d5e0e4

Co-authored-by: Michael Lindgren <mlindgren84@gmail.com>

m-lindgren mentioned this pull request Mar 5, 2023

Remove Coq.Init.Logic export almost everywhere. #1643

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Set-enriched categories #1467

Set-enriched categories #1467

umedaikiti commented Mar 6, 2022

benediktahrens commented Mar 6, 2022

umedaikiti commented Mar 7, 2022

benediktahrens commented Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

benediktahrens Mar 7, 2022

nmvdw commented Mar 7, 2022

nmvdw left a comment

nmvdw Mar 7, 2022

nmvdw Mar 7, 2022

nmvdw Mar 7, 2022

nmvdw Mar 7, 2022

nmvdw Mar 7, 2022

nmvdw Mar 7, 2022

m-lindgren left a comment

m-lindgren Nov 6, 2022

m-lindgren commented Nov 18, 2022

benediktahrens commented Nov 18, 2022

Set-enriched categories #1467

Are you sure you want to change the base?

Set-enriched categories #1467

Conversation

umedaikiti commented Mar 6, 2022

benediktahrens commented Mar 6, 2022

umedaikiti commented Mar 7, 2022

benediktahrens commented Mar 7, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nmvdw commented Mar 7, 2022

nmvdw left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

m-lindgren left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

m-lindgren commented Nov 18, 2022

benediktahrens commented Nov 18, 2022