## Stream: general

### Topic: Dealing with heq and Sigma types

#### Patrick Lutz (Nov 11 2020 at 19:49):

When proving that some type is equivalent to a Sigma type, how do you deal with heqs that pop up? Here's an example

import tactic

variables (A B : Type) (S : set A)

example : (A → B) ≃ Σ (f : S → B), {φ : A → B // ∀ (s : A) (h : s ∈ S), φ s = f ⟨s, h⟩ } :=
{ to_fun := λ g, ⟨λ s, g s.1, ⟨g, λ _ _, rfl⟩⟩,
inv_fun := λ ⟨f, φ⟩, φ.1,
left_inv := λ _, rfl,
right_inv := begin
rintros ⟨f, φ, h⟩,
ext,
{ cases x, dsimp only, tauto },
{ -- heq occurs here
sorry, }
end }


How should the final sorry be proved? By the way, this example is by Kevin Buzzard. The actual, more complicated, situation that inspired this is here if you're curious.

#### Reid Barton (Nov 11 2020 at 19:58):

Turn back and go another way

example : (A → B) ≃ Σ (f : S → B), {φ : A → B // ∀ (s : A) (h : s ∈ S), φ s = f ⟨s, h⟩ } :=
{ to_fun := λ g, ⟨λ s, g s.1, ⟨g, λ _ _, rfl⟩⟩,
inv_fun := λ p, p.2.1,
left_inv := λ _, rfl,
right_inv := begin
rintros ⟨f, φ, h⟩,
have : f = λ s, φ s.1, sorry,
subst this,
end }


ohh, nice

#### Patrick Lutz (Nov 11 2020 at 20:03):

what exactly does subst do?

#### Kevin Buzzard (Nov 11 2020 at 20:03):

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

#### Kevin Buzzard (Nov 11 2020 at 20:04):

subst takes a proof of A = B and replaces all the A's everywhere by B's, or possibly the other way around

#### Reid Barton (Nov 11 2020 at 20:04):

oh yeah, I did that just in case it would help and then forgot to mention it

#### Bryan Gin-ge Chen (Nov 11 2020 at 20:04):

(Reid's sorry can be filled with simp [h].)

#### Kevin Buzzard (Nov 11 2020 at 20:04):

it's like rw h at * except that it's more powerful because it rewrites under binders. It literally removes A from the picture.

oh, I see

#### Patrick Lutz (Nov 11 2020 at 20:05):

Kevin Buzzard said:

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

#### Reid Barton (Nov 11 2020 at 20:07):

If you look at the goal in the original right_inv it's got some _match_1 or whatever junk in it

#### Reid Barton (Nov 11 2020 at 20:08):

more importantly, the version which matches in the lambda is less likely to reduce when applied to something

#### Reid Barton (Nov 11 2020 at 20:08):

though maybe in a case as simple as this one it doesn't really matter, not sure

#### Patrick Lutz (Nov 11 2020 at 20:09):

by the way, even though the example was originally by Kevin, I was the one who introduced the angle brackets

Last updated: May 08 2021 at 09:11 UTC