Zulip Chat Archive

Stream: general

Topic: deconstruct sigma types


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Nov 30 2018 at 16:16):

nooooo

view this post on Zulip Kenny Lau (Nov 30 2018 at 16:17):

don’t deconstruct things in definitions

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 16:18):

Is this better Kenny?

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 16:19):

Or still bad?

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:19):

drop the type ascription

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 16:19):

Heh, why would this help?

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:19):

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

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 16:20):

Oh!

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:20):

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

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:20):

it's just syntax

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:21):

it's the same

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 16:21):

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

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:21):

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

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:21):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 30 2018 at 16:23):

as opposed to

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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Nov 30 2018 at 16:40):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Nov 30 2018 at 16:50):

Yeah, this is a very common fantasy on this chat

view this post on Zulip 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})

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 17:02):

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

view this post on Zulip Kevin Buzzard (Nov 30 2018 at 17:03):

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

view this post on Zulip 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