dependent functions out of a sum equivalent to ...

Stream: Is there code for X?

[Scott Morrison]

Somewhat unbelievably I can't find

def sum_fun_equiv {α β : Type*} (f : α ⊕ β → Type*) :
  (Π x, f x) ≃ (Π a, f (sum.inl a)) × (Π b, f (sum.inr b)) :=
sorry

Does anyone see it?

[Adam Topaz]

Looks like we have the non-dependent version docs#equiv.sum_arrow_equiv_prod_arrow

[Scott Morrison]

Okay. I'll add it eventually.

[Scott Morrison]

In fact, the same proof works with a tiny bit of effort, so I may try to just generalize.