Can one glue together dependent types?

Stream: mathlib4

[Terence Tao]

Given two functions (f : α → γ) (g : β → γ) with the same codomain, one can use docs#Sum.elim to glue them together into a single function Sum.elim f g: α ⊕ β → γ. For functions (f : α → α') (g : β → β') with different codomains, we can use docs#Sum.map instead to create a slightly different glued function Sum.map f g: α ⊕ β → α' ⊕ β'. For both operations one has a very convenient API (in particular, simp tends to work wonders).

But suppose now that one has two functions f: (i:α) → (α' i) g : (j:β) → (β' j) with codomains depending on the domain variable. Is there any sensible way to glue them together? I am struggling to even formulate a type to hold such a glued function. And even if one did hack together some sort of type, building an API to relate it back to the original functions looks very challenging (there are annoying cast issues as most of the solutions I came up with involved types that were only propositionally equal to the types one actually wants, rather than definitionally equal). Is there a good solution to this, or is this an inherent issue with dependent type theory?

[Aaron Liu]

Do you have any requirements for what the gluing should look like?

[Terence Tao]

I guess I should discuss the motivation. On a probability space Ω, I have one family X : (i:I) → Ω → (G i) of random variables X i, each taking values in some measurable space G i; and I have another family Y : (j:J) → Ω → (H j)of random variables Y j, taking values in some other measurable spaces H j. I would like to glue these collections into a single collection glue X Y : (k : I ⊕ J) → Ω → ??? of random variables which can be related to the original random variables; in particular, I would like iIndepFun (glue X Y) to hold if and only if iIndepFun X and iIndepFun Y both hold, and furthermore IndepFun (fun ω i ↦ X i ω) (fun ω j ↦ Y j ω) also hold. (Informally: independent samples of sets of independent variables remain jointly independent.) I could do all this when the types G i, H j were all a single type G, but am struggling to even assign a sensible type to ??? in the case when these are different.

[Aaron Liu]

since I can definitely glue them together into a function
Unit → (((i : α) → α' i) × ((j : β) → β' j))

[Yaël Dillies]

variable {α : ι → Type} {β : κ → Type} (f : ∀ i, α i) (g : ∀ j, β j)

example : ∀ iorj, Sum.elim α β iorj := Sum.rec f g

[Yaël Dillies]

You can of course insert Option.rec or any other (non-recursive) recursor, or a match instead of Sum.rec

[Terence Tao]

Ah OK. That may be the best option. There are still some issues in my application with transferring various data (e.g., [MeasureSpace]) from say α i to Sum.elim α β (Sum.inl i) (which is defeq to Sum.inl (α i)) but this is "just" a matter of applying a whole bunch of cast operators and is at least doable, albeit annoying.

[Aaron Liu]

Sum.elim α β (Sum.inl i) is defeq to α i

[Aaron Liu]

it doesn't even have the same type as Sum.inl (α i)

[Yaël Dillies]

Yes, but syntactically different, therefore typeclass search won't see through

[Yakov Pechersky]

Here's an example:

variable {α β γ : Type _} {α' : (i : α) → Type _} {β' : (j : β) → Type _} (f : (i : α) → α' i) (g : (j : β) → β' j)

variable [Inhabited α] [Inhabited β]

def sum [Inhabited α] [Inhabited β] : (ij : α ⊕ β) →
    (Σ' h : Sum.isLeft ij, α' (ij.elim id default)) ⊕ Σ' h : Sum.isRight ij, β' (ij.elim default id)
| .inl i => .inl ⟨by simp, f i⟩
| .inr j => .inr ⟨by simp, g j⟩

theorem sum_inl (i : α) : sum f g (.inl i) = .inl (⟨by simp, f i⟩) := rfl
theorem sum_inr (j : β) : sum f g (.inr j) = .inr (⟨by simp, g j⟩) := rfl

[Aaron Liu]

My point is that you won't need cast

[Yakov Pechersky]

But, yes, a naked Sum.rec works

[Terence Tao]

Oh you are using Sum.elim instead of Sum.map because α, β lie in the same universe. OK, that is a clean solution (and it would be unrealistic to expect to glue across universes anyway).

[Aaron Liu]

You can do this without messing around with types by gluing into
(α ⊕ β) → (Sigma α' ⊕ Sigma β')

[Terence Tao]

OK I see now where I went wrong. I was somehow sure that the target type needed to be Sum.map α β iorj which takes values in the ridiculous and useless space Type ⊕ Type, but this was a purely self-inflicted difficulty.