[Agda] announcing Cedille 1.0.0

[Aaron Stump]

Dear Agda community,

We are pleased to announce the public release of Cedille 1.0.0. Cedille 
implements an extrinsic pure type theory, in which datatypes with their 
induction principles can be derived as lambda encodings. The details of 
how this works are explained in several papers you can find on my web 
page (a good starting one is "From Realizability to Induction via 
Dependent Intersection").  Cedille is implemented in an Emacs mode 
communicating with a backend.  The backend is written in around 10kloc 
of Agda -- and hence we feel justified advertising on this list.  :-)

We have a Debian package for quick installation, or you can build from 
sources following some instructions (INSTALL.txt in the repo).

Cedille's web page is https://cedille.github.io.

The 1.0.0 release is tagged on github here: 
https://github.com/cedille/cedille/releases/tag/v1.0.0

Master is for development and could be broken, but the maintenance 
branch for this release (and the one you might want to checkout) is: 
https://github.com/cedille/cedille/tree/release-1.0

Sincerely, and gratefully to Agda on which this tool is based,
Aaron, for the Cedille development team
PS We welcome issues on the github issue tracker for installation 
problems or other questions.