what does the ampersand in Definitions mean, as in https://pastebin.com/Tg425qmD. Specifically, how would one translate the following to Agda : "Definition Foo := { Bar : foo1 & prod foo2 foo3 }"

this does not work to me `Definition VeridicalAdv := {Bar : nat & Foo : nat}.`

I think this is most likely kind of notation defined somewhere in library you use.

I think you could try to provide working example, then somebody may give a better answer.

Yes it is defined, it just doesn't take colon on the right. It's the syntax for dependent sums. You can try `Locate "&"`

and it will print a list of notations with `&`

that you have in scope. Including

```
Notation "{ x : A & P }" := (sigT (fun x => P)) : type_scope
(default interpretation)
```

Now you can type `About sigT`

or `Print sigT`

to learn more about it.

To translate to agda, you will have to work with agdas sigma types

thank you. another question : is there any relation between Prop in Agda (approximately proof irrelevant types) and Prop in Coq ?

agda prop is more like coq sprop

Last updated: Oct 03 2023 at 04:02 UTC