Equality of types

Stream: new members

[Simon Daniel]

Hi,
Equality of Prop can be proven by Eq.propIntro, however this does not seem to work for Types.
Ive seen a thread here where equality of types by HEq and cast was called an antipattern, but to me it seems desirable to express type equality.

variable (a b c d: Type)
variable (p: a -> b)
variable (q: b -> a)

def h: a = b := sorry

[Daniel Weber]

This is false. For example, there is a function from docs#Unit to docs#Bool - fun x => false, and from Bool to Unit - fun x => (), but Unit and Bool aren't equal

[Simon Daniel]

makes sense, but id want to proof something like this where a proper casting function exists such that p ( q x) = x for all elements:

def eq (p: ∀ (v:Option α) , v.isSome): Option α = α  := by sorry

does this mean this is unprovable?

[Joël Riou]

I have no idea what you are trying to do, but:

universe u

def eq {α : Type u} (p : ∀ (v : Option α), v.isSome) :
    Option α = α  := by
  exfalso
  simpa using p none

[Daniel Weber]

There is docs#Equiv, perhaps that's what you want?

[Edward van de Meent]

additionally, you'll be interested in docs#Subtype

[Edward van de Meent]

basically, the statement you're likely looking for is {x : Option a // x.isSome} ≃ a

[Simon Daniel]

oh yea its Equivalence that I was looking for! thanks

[Simon Daniel]

seems like zulip doesnt let me close the topic, but its resolved :)

You do not have permission to resolve topics with messages older than 7 days in this organization. Contact a moderator to resolve this topic.

[Kevin Buzzard]

Please don't resolve topics, that's the policy we use on this site.

[Simon Daniel]

I thought i was supposed to resolve topics, good to know

[Kevin Buzzard]

We'd like to switch it off completely but apparently this isn't possible

[Simon Daniel]

why do you want to disable it? these checkmarks seem like a nice indicator for finished topics

[Kevin Buzzard]

It breaks links

[Kevin Buzzard]

And we existed for years with no ability to resolve topics and people sometimes coming back to topics, and it worked fine

[Jireh Loreaux]

I recently learned on Zulip Meta that it doesn't break links anymore. They've fixed that.

[Jireh Loreaux]

@Kevin Buzzard :up: