# Zulip Chat Archive

## Stream: new members

### Topic: subtype map

#### Calle Sönne (Oct 31 2019 at 14:24):

Is there some theorem/lemma that can give me a map from a subtype into the corresponding type?

#### Rob Lewis (Oct 31 2019 at 14:25):

`subtype.val`

?

#### Calle Sönne (Oct 31 2019 at 14:26):

Thanks! I must have been searching for the wrong thing then.. thought its name would be something like 'lift' or 'map'

#### Calle Sönne (Oct 31 2019 at 14:40):

Despite its simplicity I am having problems using subtype.val

I have the following code (the only important thing is the last line in tactic mode):

open_locale classical lemma finite_prod_of_binary_prod [has_binary_products.{v} C] : ∀ (J : Type v) [fintype J], limits.has_limits_of_shape (discrete J) C | J fin := if h : nonempty J then begin let x := classical.choice h, let J' := {a // a ≠ x}, resetI, have card_lt : fintype.card J' < fintype.card J, refine fintype.card_subtype_lt J _, exact x, simp, have lim_J' : limits.has_limits_of_shape (discrete J') C, refine finite_prod_of_binary_prod J', refine ⟨_⟩, intro, let F' := discrete.lift (subtype.val J'), end else _ using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, @fintype.card x.1 x.2)⟩]}

I get the following error:

type mismatch at application J'.val term J' has type Type v : Type (max 1 (v+1)) but is expected to have type subtype ?m_3 : Type (max ? ?) state: C : Type u, 𝒞 : category C, _inst_1 : limits.has_binary_products C, finite_prod_of_binary_prod : Π (J : Type v) [_inst_2 : fintype J], limits.has_limits_of_shape (discrete J) C, J : Type v, fin : fintype J, h : nonempty J, x : J := classical.choice h, J' : Type v := {a // a ≠ x}, card_lt : fintype.card J' < fintype.card J, lim_J' : limits.has_limits_of_shape (discrete J') C, F : discrete J ⥤ C ⊢ limits.has_limit F

How do I supply the fact that J' is a subtype of J to subtype.val? Shouldnt this be inferred?

#### Chris Hughes (Oct 31 2019 at 14:43):

You can't apply `subtype.val`

to `J'`

only to an element of `J'`

#### Rob Lewis (Oct 31 2019 at 14:44):

I'm not sure what the type of `discrete.lift`

is, but note that `subtype.val`

is a function from `J'`

to `J`

, not a function that can be applied to `J'`

itself.

#### Chris Hughes (Oct 31 2019 at 14:45):

You just want `discrete.lift subtype.val`

#### Chris Hughes (Oct 31 2019 at 14:46):

Or probably `discrete.lift (subtype.val : J' -> J)`

#### Rob Lewis (Oct 31 2019 at 14:46):

You just want

`discrete.lift subtype.val`

Maybe with some type annotations.

#### Calle Sönne (Oct 31 2019 at 14:48):

Great! Thank you :)

Last updated: May 08 2021 at 04:14 UTC