# Zulip Chat Archive

## Stream: new members

### Topic: Protected inheritance

#### Nicolò Cavalleri (Jul 03 2020 at 22:22):

I do not understand how I access the fields of an inherited structure such as, in this example

```
structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)
structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)
#check bar.c
#check bar.a
#check foo.a
```

`bar.a`

#### Patrick Massot (Jul 03 2020 at 22:24):

```
structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)
structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)
#check bar.c
#check (bar.to_foo _).a
#check foo.a
set_option old_structure_cmd true
structure foo' (α : Type*) (β : Type*) :=
(a : α)
(b : β)
structure bar' (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)
#check bar'.c
#check bar'.a
#check foo'.a
```

#### Patrick Massot (Jul 03 2020 at 22:25):

But I need to go to bed, so I'll let other elaborate.

#### Nicolò Cavalleri (Jul 03 2020 at 22:26):

Patrick Massot said:

But I need to go to bed, so I'll let other elaborate.

Sure haha good night!

#### Mario Carneiro (Jul 03 2020 at 22:27):

```
structure foo (α : Type*) (β : Type*) :=
(a : α)
(b : β)
structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β :=
(c : γ)
variables (α β γ : Type) (x : foo α β) (y : bar α β γ)
#check y.c
#check y.a -- y.to_foo.a : α
#check x.a
```

#### Nicolò Cavalleri (Jul 03 2020 at 22:32):

Mario Carneiro said:

`structure foo (α : Type*) (β : Type*) := (a : α) (b : β) structure bar (α : Type*) (β : Type*) (γ : Type*) extends foo α β := (c : γ) variables (α β γ : Type) (x : foo α β) (y : bar α β γ) #check y.c #check y.a -- y.to_foo.a : α #check x.a`

I am not sure I understand why your example works but in any case I still cannot make the following example work:

```
import topology.algebra.group
structure topological_group_morphism
(G : Type*) [topological_space G] [group G] [topological_group G]
(G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' :=
(continuous_to_fun : continuous to_fun)
instance {G : Type*} [topological_space G] [group G] [topological_group G]
{G' : Type*} [topological_space G'] [group G'] [topological_group G'] :
has_coe_to_fun (topological_group_morphism G G') := ⟨_, (topological_group_morphism.to_monoid_hom _).to_fun⟩
```

#### Jalex Stark (Jul 03 2020 at 22:48):

I think this works

```
import topology.algebra.group
structure topological_group_morphism
(G : Type*) [topological_space G] [group G] [topological_group G]
(G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' :=
(continuous_to_fun : continuous to_fun)
instance {G : Type*} [topological_space G] [group G] [topological_group G]
{G' : Type*} [topological_space G'] [group G'] [topological_group G'] :
has_coe_to_fun (topological_group_morphism G G') :=
⟨_, λ a, a.to_fun⟩
```

#### Nicolò Cavalleri (Jul 03 2020 at 22:50):

Jalex Stark said:

I think this works

`import topology.algebra.group structure topological_group_morphism (G : Type*) [topological_space G] [group G] [topological_group G] (G' : Type*) [topological_space G'] [group G'] [topological_group G'] extends monoid_hom G G' := (continuous_to_fun : continuous to_fun) instance {G : Type*} [topological_space G] [group G] [topological_group G] {G' : Type*} [topological_space G'] [group G'] [topological_group G'] : has_coe_to_fun (topological_group_morphism G G') := {F := _, G → G', coe := λ a, a.to_fun}`

Ok thanks this makes some sense! I'll try to understand the details tomorrow!

#### Jalex Stark (Jul 03 2020 at 22:51):

sorry, the version you quoted has a typo that makes it not work. The current version compiles on my end, though, and seems very similar to what you had written

#### Nicolò Cavalleri (Jul 03 2020 at 22:52):

Sure I saw the correction ;)

#### Nicolò Cavalleri (Jul 03 2020 at 22:55):

Jalex Stark said:

sorry, the version you quoted has a typo that makes it not work. The current version compiles on my end, though, and seems very similar to what you had written

Thanks a lot!

Last updated: May 13 2021 at 17:42 UTC