Sets or types? Or both?

Stream: new members

[N Gelwan]

New to lean4. I'm looking to get my feet wet by implementing the content of https://link.springer.com/book/10.1007/978-1-4471-0009-6.

I'm trying to figure out what foundational "API" I should use; as far as I've gotten through the text, the material has been tacitly framed in terms of sets, but I'm wondering whether I should try to frame everything in terms of types, since there seems to be more native "facilities" for speaking that language in lean4. Any tips on how to proceed?

I've been playing around with Mathlib.Init.Set and the facilities that it offers for coercing sets into types, but from my initial experiments it seems like maybe this doesn't completely translate the idioms between the two frameworks, which is reasonable, but I can't tell what might be missing, and whether this translation is going to be introducing an overhead into all of my constructions. Or maybe I'm missing something, and this is a moot point? Please advise.

I should note that I am familiar with lean's modelling of sets as elements of a type which satisfy a proposition. I'm not sure if I'm leveraging that model effectively, though.

[N Gelwan]

For example; representing a structure with an operation which is framed in the book as taking elements of one set to subsets of another.

I could write that as a typeclass in two ways:

import Mathlib.Init.Set

class Domainable\1 (\a : Type) (\b : Type) where
  domain : \a \r Set \b

class Domainable\2 (\a : Type) {\b : Type) (s : Set \b) where
  domain: \a \r \powerset s

Is there any reason why I'd do the latter? It seems verbose.

[Luigi Massacci]

As a first thing, as explained in #backticks if you add “lean” after the backticks you’ll get lean syntax highlighting for the code and the ability to open it on the lean web editor. Beyond that, I’m not an expert, but the latter doesn’t seem right. I doubt it would type check: the codomain of your second function is not a type, (which it should be) but rather a term of type Set (Set β), and even if it were well typed it would not be the same as the one above unless you took s to be univ.

And to answer your question I think (?) the first is what you want.

[Kyle Miller]

The first one is more general in a sense -- you can always pass in a set as the second argument to Dominable\1, but the second requires a set (so you need to pass in Set.univ to recover something equivalent to the first definition).

[Kyle Miller]

(@Luigi Massacci The Set type has a coercion to Type using Subtype, so the codomain \powerset s is ends up being interpreted as something that's defeq to {x // x \in \powerset s}. The actual term has Set.Elem wrapped around it, but that's an identity function, and it's used for pretty printing and some other automation.)

[Luigi Massacci]

Ahh I see, learned something new today. Sorry @N Gelwan for the fake news