coercion from a Pi Subtype

Stream: Is there code for X?

[Yoh Tanimoto]

which is the most natural way to get an object from Pi of Subtypes to an object of Pi of the original types?

import Mathlib

variable {ι : Type} {G : ι → Type} [∀ i, Group (G i)] (H : (i : ι) → Subgroup (G i)) (i : ι)
variable (x : (i : ι) → H i)

#check (fun i => (x i) : (i : ι) → G i) -- works
#check (x : (i : ι) → G i) -- fails

[Yoh Tanimoto]

cf.

import Mathlib

variable (G1 G2 : Type) [Group G1] [Group G2] (H1 : Subgroup G1) (H2 : Subgroup G2)
variable (z : H1 × H2)

#check (⟨z.fst, z.snd⟩ : G1 × G2) -- works
#check (z : G1 × G2) -- fails

[Yoh Tanimoto]

does it make sense to have these coercions?

[Junyan Xu]

fun i ↦ (x i : G i) or fun i ↦ (x i).val should work

[Yoh Tanimoto]

yes, but do I have to write that way every time?

[Edward van de Meent]

You can use the shorter (x · |>.val) instead, if that helps...

[Yoh Tanimoto]

not sure, is it a bad idea to have these coercions? if so, why?

[Edward van de Meent]

i think having coercion instance might be bad, because it gives multiple phrasings of the same term, e.g. in the Pi example, should we write (coe x) i or coe (x i)? additionally, when x is some lambda, the term will look particularly bad...

[Aaron Liu]

Edward van de Meent said:

e.g. in the Pi example, should we write (coe x) i or coe (x i)?

we should never be explicitly writing coe

[Edward van de Meent]

yes, i agree, but this was just to highlight the difference

[Yoh Tanimoto]

I see the question, what happens if I added a coercion instance with low priority? then shouldn't coe (x i) be applied first?

[Eric Wieser]

Note that you can also write #check ((x ·) : (i : ι) → G i)

[Edward van de Meent]

(those inner brackets are redundant: #check (x · : (i : ι) → G i))

[Yoh Tanimoto]

thanks to you all for your replies.

I think, for what I want to do, I should have used Subgroup.pi instead of just Pi (the latter of which has also a Group instance but I wanted it to be a subgroup).

import Mathlib

variable {ι : Type} {G : ι → Type} [∀ i, Group (G i)] (H : (i : ι) → Subgroup (G i)) (i : ι)
variable (x : Subgroup.pi (Set.univ : Set ι) H) (i : ι)

#check (x : (i : ι) → G i)
#check x.val i