non-dependent type sheaves

Stream: maths

[Kevin Buzzard]

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]

CommRing is a dependent type

[Yury G. Kudryashov]

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

[Kevin Buzzard]

Yury G. Kudryashov said:

CommRing is a dependent type

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

[Yury G. Kudryashov]

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

[Nick Chopper]

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]

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

[Kevin Buzzard]

bundled categories

[Nick Chopper]

@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]

(deleted)

[Nick Chopper]

sorry for poor english