Zulip Chat Archive

Stream: maths

Topic: non-dependent type sheaves


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:57):

CommRing is a dependent type

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 08:57):

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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Apr 01 2020 at 09:48):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 02 2020 at 10:54):

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

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 11:35):

bundled categories

view this post on Zulip 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))

view this post on Zulip Nick Chopper (Apr 02 2020 at 12:12):

(deleted)

view this post on Zulip Nick Chopper (Apr 02 2020 at 12:12):

sorry for poor english


Last updated: May 11 2021 at 15:12 UTC