Extending an abbreviated structure

Stream: maths

[Bhavik Mehta]

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?

[Bhavik Mehta]

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

[Bhavik Mehta]

I suppose I could minimise the example more:

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

class foo α extends baz α.

[Yury G. Kudryashov]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

Though I might be missing something in your description

[Yury G. Kudryashov]

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

[Bhavik Mehta]

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

[Yury G. Kudryashov]

How should cartesian_closed deduce category and has_finite_products?

[Bhavik Mehta]

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

[Yury G. Kudryashov]

I don't see these arguments in your example.

[Bhavik Mehta]

Ah sorry my mistake

[Bhavik Mehta]

Corrected version:

[Bhavik Mehta]

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

[Bhavik Mehta]

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

[Yury G. Kudryashov]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

The obvious fix for that is to just include that line

[Bhavik Mehta]

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