'Prop' in definitions

Stream: new members

[Holly Liu]

why do set and equivalence relations map to a Prop in their definitions: def set (α : Type u) := α → Prop and constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u where r : (α → α → Prop)?

[Kevin Buzzard]

What is your definition of an equivalence relation, if it doesn't involve true-false statements?

[Kevin Buzzard]

The answer to the set question is that lean identifies a subset S of X with the function that sends an element x of X to the true-false statement $x\in S$

[Kevin Buzzard]

Although it's probably worth remarking that using this fact is breaking the abstraction barrier

[Holly Liu]

Kevin Buzzard said:

breaking the abstraction barrier

is that like what the end-user is not supposed to see?

[Holly Liu]

Kevin Buzzard said:

What is your definition of an equivalence relation, if it doesn't involve true-false statements?

i think the (α → α → Prop) is a bit confusing. i'm not sure what the first two α's are for

[Kevin Buzzard]

I'm asking you what your definition of an equivalence relation on alpha is. It should be exactly the same, or obviously equivalent, to Lean's, but you're not saying what you think it is so it's difficult to make progress

[Adam Topaz]

If you identify set A with A -> Prop, then A -> A -> Prop (which really means A -> (A -> Prop) becomes A -> (set A), i.e. a function which associates to any element of A a subset of A. One way to think about this is by saying that this function sends a : A to the "set of all elements which are related to a"

[Adam Topaz]

There are other ways to grok this, but as Kevin said, it would be helpful to know how you usually define a relation

[Nicholas]

doesnt the equivalence relation $r$ take two $\alpha$ as arguments and return whether or not they are equivalent (which is a proposition)?

[Holly Liu]

Kevin Buzzard said:

I'm asking you what your definition of an equivalence relation on alpha is. It should be exactly the same, or obviously equivalent, to Lean's, but you're not saying what you think it is so it's difficult to make progress

sorry, my definition was that an equivalence relation on alpha is something that satisfies three properties, which are reflexivity, symmetry, and transitivity. i meant to say that i didn't understand why it was defined without these properties, but i see that it can be thought of as mapping each element of a set to "a set of all elements which are related to the element", and that it's checking for equivalence between two arguments.

[Kevin Buzzard]

Yes, that's correct: but your question was about the "something", not about the axioms. The thing you quoted above is not an equivalence relation, it's just a binary relation.

[Eric Wieser]

The other piece of the puzzle is that quot effectively takes the closure of the relation you pass it using docs#eqv_gen

[Holly Liu]

i didn't realize it was just a binary relation. i may have confused binary relation with equivalence relations

[Eric Wieser]

docs#quotient is the version that takes an equivalence relation to begin with

[Holly Liu]

oh, equivalence relations are setoids?

[Eric Wieser]

Well, strictly an equivalence relation is any relation that satisfies docs#equivalence

[Holly Liu]

ah ok

[Esteban Estupinan]

hi all, I m I am examining in more detail the creation of definitions in lean and I have seen small differences in the type here some examples

def upper_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, s ≤ b }
def lower_bounds (S : set ℝ) : set ℝ := { b | ∀s ∈ S, b ≤ s }
def is_least (S : set ℝ) (l : ℝ) : Prop := l ∈ S ∧ l ∈ lower_bounds S
def is_lub (S : set ℝ) (l : ℝ) : Prop := is_least (upper_bounds S) l

def S (x y : A) := R x y ∧ R y x

I ask you, when we should use the Prop type, when we should not use any type, how does each one vary, thank you very much for your time

[Kyle Miller]

When you leave off the type, Lean will infer it if it can (if it can't it will show an error). This should be exactly the same:

def S (x y : A) : Prop := R x y ∧ R y x

Try doing

#check S

to see what type Lean has inferred.

[Kyle Miller]

(I personally think it's nicer to include the : Prop, but you don't have to.)