Zulip Chat Archive

Stream: maths

Topic: non-dependent type sheaves


Kevin Buzzard (Apr 01 2020 at 08:53):

I guess this is well-known but it's only just dawned on me. Rings are set up in a semi-bundled way in mathlib. So a sheaf of rings needs to involve a dependent type, because it's F : opens X -> Type followed by [hF : Pi (U : opens X), comm_ring (F U)]. But if rings were completely bundled then we could just have F : opens X -> CommRing and no dependent type is needed. Does this mean I should switch to Isabelle or are there dependent types under the hood in this setting?

Yury G. Kudryashov (Apr 01 2020 at 08:57):

CommRing is a dependent type

Yury G. Kudryashov (Apr 01 2020 at 08:57):

Disclaimer: I never tried Isabelle, and I don't know what it can (not) handle.

Kevin Buzzard (Apr 01 2020 at 09:13):

Yury G. Kudryashov said:

CommRing is a dependent type

I see. I thought it might well be something like this.

Yury G. Kudryashov (Apr 01 2020 at 09:48):

Another example: we have several measurable_space instances defined to be top.

Nick Chopper (Apr 02 2020 at 10:08):

I create this(cat.lean) several days ago and have some initial thoughts. I think it might possible to create one completely bundled structure and then get all sorts of things (unbundled structure, like cat/cat'/cat'/... in the file, and proof of equivalence between them or something else) automatically.

Johan Commelin (Apr 02 2020 at 10:54):

@Nick Chopper Sorry, I'm a bit dense... what exactly is your proposal?

Kevin Buzzard (Apr 02 2020 at 11:35):

bundled categories

Nick Chopper (Apr 02 2020 at 12:12):

@Johan Commelin auto coe between bundled/unbundled structure (loop?), so as to use type class fill in unbundled one and then actually get a bundled one. I find it has been solved by category_theory.bundled in the case of one-parameter class, but I wonder if it is possible to generate code like inductive type (say, unbundled structure from bundled (don't know how to avoid name confliction (instead of adding ') yet))

Nick Chopper (Apr 02 2020 at 12:12):

(deleted)

Nick Chopper (Apr 02 2020 at 12:12):

sorry for poor english


Last updated: Dec 20 2023 at 11:08 UTC