[Agda] origin of "Agda"?

[Peter Selinger]

Thanks for the information! That answer was more colorful that I
expected! Of course I immediately spent an hour looking up Agda the
Hen videos on YouTube. I even found some in English.

Agda is in good company, as far as words with raunchy etymology go.
Have you ever looked up the origin of the word "porcellain"? It is
related to "pork", but with an interesting detour.

-- Peter

Andreas Abel wrote:
> 
> Unfortunately, the account given by Vilhelm is correct, although we try 
> to keep this embarrassing part of history under the carpet... :D
> 
> Certainly a pun / antithesis to Coq.
> 
> On 06.07.2016 21:51, Vilhelm Sjoberg wrote:
> > Agda is a female given name in Swedish. I've heard claims that the name
> > of the computer language is a reference to the humorous song "Hönan
> > Agda" [Agda the hen] by Cornelis Vreeswijk. A companion for Coq, as it were.
> >
> > Vilhelm
> >
> > On Wed, Jul 6, 2016 at 3:03 PM, Peter Selinger <selinger at mathstat.dal.ca
> > <mailto:selinger at mathstat.dal.ca>> wrote:
> >
> >     Does anyone know why Agda is called Agda? I realize the name is based
> >     on the 1999 "Agda 1" by Catarina Coquand, but what was the meaning of
> >     the original name? Is it an acronym (I noticed that some of the early
> >     papers spell it AGDA)? Or is it someone's name? I looked at some of
> >     the Agda 1 materials, but found no explanation.
> >
> >     Just curious, -- Peter