# Zulip Chat Archive

## Stream: new members

### Topic: symmetric function

#### Vaibhav Karve (Mar 22 2020 at 15:11):

I have the following setup:

example : (A B : Sort) (rel : A -> A -> B) : Prop := forall a b : A, f a b = f b a

In the special case of `B`

being `Prop`

, I know that I can restate the above as `symmetric f`

. Is there a corresponding general version of `symmetric`

that will work for any `B`

?

I also discovered that for some reason, library search doesn't work:

example : (A : Sort) : (A -> A -> Prop) -> Prop := by suggest -- doesn't work example : (A : Sort) : (A -> A -> Prop) -> Prop := by library_search -- doesn't work

#### Mario Carneiro (Mar 22 2020 at 15:14):

That looks like `commutative`

#### Mario Carneiro (Mar 22 2020 at 15:15):

but that might also be special cased to `B = A`

#### Mario Carneiro (Mar 22 2020 at 15:17):

I think that whole section of core is due for an update

#### Vaibhav Karve (Mar 22 2020 at 15:30):

Yes, `commutative`

is close but not quite right. I definitely want `B ≠ A`

. Any idea why the `suggest`

doesn't work?

#### Kevin Buzzard (Mar 22 2020 at 16:00):

What is `Sort`

by the way? Isn't it defeq to `Prop`

or something?

#### Mario Carneiro (Mar 22 2020 at 16:17):

it is `Prop`

#### Mario Carneiro (Mar 22 2020 at 16:17):

#check Sort -- Prop : Type

#### Mario Carneiro (Mar 22 2020 at 16:18):

Technically `Prop`

is a notation for `Sort`

:

notation `Prop` := Sort 0

#### Kevin Buzzard (Mar 22 2020 at 16:37):

@Vaibhav Karve are you aware of this? You say "in the special case of `B`

being `Prop`

" but `Prop`

is not allowed as a value for `B`

in what you say, strictly speaking.

#### Vaibhav Karve (Mar 22 2020 at 18:46):

Yes, Kevin, I was aware of this. In my attempt to write a MWE, I went too far. I was actually looking for a simple analogue of `symmetric`

that would work for `Sort u`

, not just `Sort`

.

#### Mario Carneiro (Mar 22 2020 at 18:54):

You can just write `Sort*`

if you don't want to declare the universe - or even nothing at all, that is:

example (A B) (rel : A -> A -> B) : Prop := forall a b : A, f a b = f b a

This is my favorite way to write theorems. It's compact, maximally general and there is nothing to mess up

#### Vaibhav Karve (Mar 22 2020 at 19:14):

Thanks for teaching me this new trick. I did not know that omitting the type is the same as writing `Sort*`

(provided there aren't other type-inferences, ofcourse).

Last updated: May 11 2021 at 22:14 UTC