Zulip Chat Archive

Stream: maths

Topic: Extending an abbreviated structure


view this post on Zulip Bhavik Mehta (Jun 16 2020 at 23:46):

import category_theory.closed.cartesian

universes v u
variable (C : Type u)

namespace category_theory
open category_theory.limits

class foo extends has_finite_limits.{v} C, has_finite_colimits.{v} C, cartesian_closed.{v} C.

end category_theory

This fails, with the message complaining that cartesian_closed isn't a structure (it's an abbreviation for a structure); how can I get this to work?

view this post on Zulip Bhavik Mehta (Jun 16 2020 at 23:46):

Or is the only option to make it a field and mark the deconstructors as attributes

view this post on Zulip Bhavik Mehta (Jun 16 2020 at 23:54):

I suppose I could minimise the example more:

class bar (n : ) (α : Type).
abbreviation baz := bar 1

class foo α extends baz α.

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 02:26):

In linear algebra we extend the original structure (e.g., extends semimodule instead of extends vector_space).

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:28):

But that's not good enough in this case, since cartesian_closed is a special case of monoidal_closed with a specific typeclass argument

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:29):

Though I might be missing something in your description

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 02:32):

Could you please copy+paste or link the definitions you're talking about?

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:33):

https://github.com/leanprover-community/mathlib/blob/a19dca67c228f784c9a3321106b939953a6f83ba/src/category_theory/closed/cartesian.lean#L77

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 02:37):

How should cartesian_closed deduce category and has_finite_products?

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:38):

I'm not sure what you mean by that...

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 02:39):

I don't see these arguments in your example.

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:41):

Ah sorry my mistake

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:41):

Corrected version:

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:41):

import category_theory.closed.cartesian

universes v u

namespace category_theory
open category_theory.limits

variables (C : Type u) [category.{v} C]

class foo extends has_finite_limits.{v} C, has_finite_colimits.{v} C, cartesian_closed.{v} C.

end category_theory

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:41):

has_finite_products is inferred from has_finite_limits which is in mathlib somewhere in the import

view this post on Zulip Yury G. Kudryashov (Jun 17 2020 at 02:55):

Have you tried using monoidal_closed in the definition? Can it prove cartesian_closed from foo by apply_instance in this case?

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:56):

I expect no because of https://github.com/leanprover-community/mathlib/blob/a19dca67c228f784c9a3321106b939953a6f83ba/src/category_theory/closed/cartesian.lean#L38

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:56):

The obvious fix for that is to just include that line

view this post on Zulip Bhavik Mehta (Jun 17 2020 at 02:57):

But that would mean I'd need that line in any file where I use foo


Last updated: May 06 2021 at 18:20 UTC