## Stream: general

### Topic: deconstruct sigma types

#### Kevin Buzzard (Nov 30 2018 at 16:16):

-- works fine
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (x : (Σ (a : α), f a)), x.1

-- doesn't work
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (⟨s,t⟩ : (Σ (a : α), f a)), s
-- invalid binder, identifier expected
-- and other errors


Can't I take a sigma type apart like this? Isn't a sigma type just a structure? I suspect I'm missing a trick?

nooooo

#### Kenny Lau (Nov 30 2018 at 16:17):

don’t deconstruct things in definitions

#### Kevin Buzzard (Nov 30 2018 at 16:18):

-- works
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ (x : (Σ (a : α), f a)), let ⟨s,t⟩ := x in s


#### Kevin Buzzard (Nov 30 2018 at 16:18):

Is this better Kenny?

#### Mario Carneiro (Nov 30 2018 at 16:19):

drop the type ascription

#### Kevin Buzzard (Nov 30 2018 at 16:19):

Heh, why would this help?

#### Mario Carneiro (Nov 30 2018 at 16:19):

the syntax for lambda match is λ ⟨s,t⟩, ... with no type ascriptions permitted

Oh!

#### Mario Carneiro (Nov 30 2018 at 16:20):

the ⟨s,t⟩ is not actually a pair even though it looks like one

it's just syntax

#### Kevin Buzzard (Nov 30 2018 at 16:20):

Kenny says it's a bad idea -- is the let thing OK or is it a bad idea for the same reason?

it's the same

#### Kevin Buzzard (Nov 30 2018 at 16:21):

-- works
example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ ⟨s,t⟩, s


#### Mario Carneiro (Nov 30 2018 at 16:21):

The simpler way is just to pattern match right from the start

#### Mario Carneiro (Nov 30 2018 at 16:21):

example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α
| ⟨s,t⟩ := s


#### Mario Carneiro (Nov 30 2018 at 16:22):

I think the reason Kenny doesn't like those definitions is because it creates an auxiliary, and it doesn't unfold unless it's an explicit pair

#### Mario Carneiro (Nov 30 2018 at 16:23):

as opposed to

example (α : Type) (f : α → Type) :
(Σ (a : α), f a) → α :=
λ p, p.1


#### Johan Commelin (Nov 30 2018 at 16:40):

It would be nice if what Kevin wants would just be syntactic sugar for the p, p.1 version...

#### Johan Commelin (Nov 30 2018 at 16:40):

But I guess syntactic sugar will only take you so far...

#### Mario Carneiro (Nov 30 2018 at 16:49):

this is a thing: they are called lazy pattern matches in haskell, and they've been discussed on this chat before

#### Patrick Massot (Nov 30 2018 at 16:50):

Yeah, this is a very common fantasy on this chat

#### Kevin Buzzard (Nov 30 2018 at 17:02):

Reality: set.image (λ x, let (⟨⟨⟨j,k⟩,f⟩,r⟩ : (Σ y : (Σ x : J × J, (R x.1) → (R x.2)), R y.1.1)) := x in (X ⟨j,r⟩ - X ⟨k,f r⟩)) {x | x.1 ∈ F})

#### Kevin Buzzard (Nov 30 2018 at 17:02):

well, that's actually just a small piece of the reality

#### Kevin Buzzard (Nov 30 2018 at 17:03):

We're making colimits in the category of commutative rings!

#### Kevin Buzzard (Nov 30 2018 at 17:04):

Without it, it will be x.1.1.1 everywhere

Last updated: May 15 2021 at 00:39 UTC