# Zulip Chat Archive

## Stream: maths

### Topic: Extending an abbreviated structure

#### 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?

#### Bhavik Mehta (Jun 16 2020 at 23:46):

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

#### 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 α.
```

#### 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`

).

#### 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

#### Bhavik Mehta (Jun 17 2020 at 02:29):

Though I might be missing something in your description

#### Yury G. Kudryashov (Jun 17 2020 at 02:32):

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

#### Bhavik Mehta (Jun 17 2020 at 02:33):

#### Yury G. Kudryashov (Jun 17 2020 at 02:37):

How should `cartesian_closed`

deduce `category`

and `has_finite_products`

?

#### Bhavik Mehta (Jun 17 2020 at 02:38):

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

#### Yury G. Kudryashov (Jun 17 2020 at 02:39):

I don't see these arguments in your example.

#### Bhavik Mehta (Jun 17 2020 at 02:41):

Ah sorry my mistake

#### Bhavik Mehta (Jun 17 2020 at 02:41):

Corrected version:

#### 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
```

#### 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

#### 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?

#### 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

#### Bhavik Mehta (Jun 17 2020 at 02:56):

The obvious fix for that is to just include that line

#### 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