map from sigma type

Stream: general

[Kevin Buzzard]

aargh I can't figure out a basic type theory thing. As part of LTE I want to relate binary sums to sigma types over a type with two terms, but I'm failing to write down the map from the sigma type to the binary sum:

import tactic

variables S T : Type

def X : bool → Type
| ff := S
| tt := T

def foo : Σ a, X S T a → S ⊕ T := -- the obvious map, sending (ff,s) to s and (tt,t) to t
λ x, @sigma.rec bool (X S T) (λ _, S ⊕ T) (λ b st, @bool.rec (λ _, S ⊕ T) (sum.inl st) (sum.inr st)) x
/-
type mismatch at application
  sum.inl st
term
  st
has type
  X S T b
but is expected to have type
  S
-/

Ideally I'd like to avoid the equation compiler because I'm doing this as a let in the middle of a tactic proof, but I could just break this definition out if necessary.

[Eric Wieser]

Fwiw, X is docs#cond

[Eric Wieser]

And if you're lucky we have docs#equiv.sum_equiv_sigma_bool

[Kevin Buzzard]

aah got it -- docs#sum_equiv_sigma_bool

[Kevin Buzzard]

so the key is to use match, which seems to me to somehow be strictly more powerful than sigma.rec the way I was using it because it forces x.2 to have the right type. Nice!

[Eric Rodriguez]

it also parses as Σ a, (X S T a → S ⊕ T) the way you wrote it, fyi

[Kevin Buzzard]

fortunately that wasn't true in my actual use case but thanks!

[Eric Rodriguez]

in your original code, this seems to work:

def foo : (Σ a, X S T a) → S ⊕ T := -- the obvious map, sending (ff,s) to s and (tt,t) to t
@sigma.rec _ _ (λ _, S ⊕ T) (λ b, @bool.rec_on (λ b, X S T b → S ⊕ T) b sum.inl sum.inr)

was a super pain to get the elaborator to work, though; I did it in tactic mode, turned on pp.all and show_term, and then worked backwards removing what could be removed and not what couldn't

[Kevin Buzzard]

Aah I had the motive wrong! no that's not it -- you moved st after the colon, that's the trick I was missing.

[Kevin Buzzard]

Yeah with that trick you don't even need the @s, like in the match case:

def foo' : (Σ a, X S T a) → S ⊕ T :=
λ x, sigma.rec (λ b, bool.rec (sum.inl) (sum.inr) b) x

Thanks!

[Kyle Miller]

Kevin Buzzard said:

so the key is to use match, which seems to me to somehow be strictly more powerful than sigma.rec the way I was using it because it forces x.2 to have the right type. Nice!

For those following along (like me), this is a match that implements it:

def foo'' : (Σ a, X S T a) → S ⊕ T
| ⟨ff, x⟩ := sum.inl x
| ⟨tt, y⟩ := sum.inr y

[Kevin Buzzard]

Yeah, I didn't try pattern matching with my original goal because I was in the middle of a proof, and pattern matching failed when I tried in my example above because of my bracket fail :D