## Stream: general

### Topic: is this choice computable?

#### Kenny Lau (Sep 04 2018 at 12:29):

Can the two sorrys be filled in?

variables (ι : Type*) (β : ι → Type*) [Π i, has_zero (β i)]

def pointed_sigma.aux : Type* :=
option Σ i, β i

inductive pointed_sigma.r : pointed_sigma.aux ι β → pointed_sigma.aux ι β → Prop
| refl : Π x, pointed_sigma.r x x
| zero_left : Π i, pointed_sigma.r none (some ⟨i, 0⟩)
| zero_right : Π i, pointed_sigma.r (some ⟨i, 0⟩) none
| zero : Π i j, pointed_sigma.r (some ⟨i, 0⟩) (some ⟨j, 0⟩)

instance pointed_sigma.setoid : setoid (pointed_sigma.aux ι β) :=
{ r := pointed_sigma.r ι β,
iseqv := begin
refine ⟨λ x, _, λ x y h, _, λ x y z h1 h2, _⟩,
{ constructor },
{ cases h; constructor },
{ cases h1; cases h2; constructor }
end }

def pointed_sigma : Type* :=
quotient (pointed_sigma.setoid ι β)

namespace pointed_sigma

instance : has_zero (pointed_sigma ι β) :=
⟨⟦none⟧⟩

def of (i : ι) (x : β i) : pointed_sigma ι β :=
⟦some ⟨i, x⟩⟧

def choice : Π (i j : ι) (x : β i) (H : ∃ y, of ι β i x = of ι β j y), β j := sorry
theorem choice_eq (i j : ι) (x : β i) (H) : of ι β i x = of ι β j (choice ι β i j x H) := sorry

end pointed_sigma


#### Kenny Lau (Sep 04 2018 at 12:30):

So I have a bunch of pointed types, indexed by the type ι.

#### Kenny Lau (Sep 04 2018 at 12:30):

I'm building the pointed union of these pointed types.

#### Kenny Lau (Sep 04 2018 at 12:30):

(The point is represented by zero.)

#### Kenny Lau (Sep 04 2018 at 12:31):

So for each i : ι, I have a function from the pointed set indexed by i to the union.

#### Kenny Lau (Sep 04 2018 at 12:31):

I'm wondering if I can reverse this operation, i.e. given an element of the pointed union, with a proof that it is from some element of the pointed set indexed by i, I would like to give back this element of the pointed set.

#### Reid Barton (Sep 04 2018 at 13:58):

I suspect you need decidable equality on I

#### Kenny Lau (Sep 04 2018 at 14:02):

that's also what I suspect, but I can't prove

Last updated: Aug 03 2023 at 10:10 UTC