Search engine support

[fredrik-bakke]

The library still appears in this less-than-favorable form in Google's search results:

There's a few issues to point out that could be improved.

1. The site title is "Github Pages" rather than "agda-unimath"
2. The favicon is not displayed
3. The preview content is gibberish.

[VojtechStep]

I don't think we can do much about the favicon, unfortunately, as long as agda-unimath is hosted at https://unimath.github.io/agda-unimath/ — quoting Google documentation, we're restricted by:

Google Search only supports one favicon per site, where a site is defined by the hostname. For example, https://www.example.com/ and https://code.example.com/ are two different hostnames, and therefore can have two different favicons. However, https://www.example.com/sub-site is a subdirectory of a site, and you can only set one favicon for https://www.example.com/, which applies to the site and its subdirectories.

Since we're a subdirectory of unimath.github.io, our favicon is set by unimath.github.io; there is currently no favicon for that, and it would set one for both agda-unimath and UniMath.

The third point about "preview content" (usually called "description") is tricky. Best we could do is set a <meta> description tag, but search engines rarely respect those. See Google's documentation:

Snippets are primarily created from the page content itself. However, Google sometimes uses the meta description HTML element if it might give users a more accurate description of the page than content taken directly from the page.

Emphasis might*. I doubt Google can properly judge what is an accurate description of a literate Agda file. My experience is that the search engines will just put whatever they want in there — I checked search results on some websites with proper description tags, and DuckDuckGo, Google and Bing all show different snippets from the page; none of them show the description tag text.

[fredrik-bakke]

Thank you so much for the helpful comment! I just submitted a PR where the site name is specified both in structured data markup and with open graph tags. Moreover, it gives search engines and other link-rendering services pointers to the agda-unimath logo we have hosted, as well as our search feature.