[Agda] Blog post: The Agda's New Sorts

[Henning Basold]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA512

Hi Jesper,

Do you think it would make sense and be feasible to implement
anonymous universes à la Harper and Pollack in Agda?

Robert Harper and Robert Pollack. Type checking with universes.
Theoretical Computer Science, 89:107-136, 1991.

Cheers,
Henning

On 15/05/18 19:09, Thorsten Altenkirch wrote:
> Hi jesper,
> 
> I appreciate your efforts to make universes more flexible and
> maybe capture other notions of universe than the ones given by
> size. However, I have another issue with the current mechanism
> (which I actually proposed many years ago). I don't like that all
> definitions are cluttered with these pesky level annotations. When
> teaching an introductory course I don't really want to talk about
> levels but on the other hand I would like to use the definitions
> from the standard library and not my own simplified versions.
> However, whenever I show a library definition I have to instruct
> them to ignore all those levels for the time being.
> 
> Is there a way out of this dilemma? Coq only does fully automatic 
> indexing but there are many situation where this is not what you
> want. Is there a way to infer levels and automatically add level
> annotations but be still able to do the explicitly if you want (or
> need) to?
> 
> Cheers, Thorsten
> 
> From: Agda <agda-bounces at lists.chalmers.se 
> <mailto:agda-bounces at lists.chalmers.se>> on behalf of Jesper Cockx 
> <Jesper at sikanda.be <mailto:Jesper at sikanda.be>> Date: Friday, 4 May
> 2018 at 09:45 To: agda list <agda at lists.chalmers.se
> <mailto:agda at lists.chalmers.se>> Subject: [Agda] Blog post: The
> Agda's New Sorts
> 
> Hi all,
> 
> Yesterday I posted a blog post on the recent work I did on Agda's 
> handling of sorts. You can read it here: 
> https://jesper.sikanda.be/posts/agdas-new-sorts.html
> 
> Any comments are very welcome here on this list!
> 
> Cheers, Jesper
> 
> 
> This message and any attachment are intended solely for the
> addressee and may contain confidential information. If you have
> received this message in error, please contact the sender and
> delete the email and attachment.
> 
> Any views or opinions expressed by the author of this email do not 
> necessarily reflect the views of the University of Nottingham.
> Email communications with the University of Nottingham may be
> monitored where permitted by law.
> 
> 
> 
> 
> 
> _______________________________________________ Agda mailing list 
> Agda at lists.chalmers.se 
> https://lists.chalmers.se/mailman/listinfo/agda
> 
-----BEGIN PGP SIGNATURE-----

iQIzBAEBCgAdFiEEMnUmuprSDishxVMiatBsEc2xMm4FAlr73ggACgkQatBsEc2x
Mm4hgA//SIhOgEq2b80/yioVsTlglqzseaonHmH3OAULT15yrLIyHNJ0uWSkFmB8
nfOoiIdpOYFg4Xrq7Bc3zSl0Fa1yLBfx3AOPLE267/BrZvQmdjn/Kzh1MkVJMNRT
rdfgRD7mCt0UaMGWX2PuoTsh3FqpZ/LXe+R6GIGSWen7yr8ByG85Hd509WgLZ+sM
TQlPcHn7aebdfJ2GWRwxjab66dySnGRxZ/rRiAFJWsepl7Z5tohsfjdvZ3TCVAOw
URDTGOAO/opD8nlpz0CeSyt0dl+qr+uem9Ofphd6s7R67PEI4WuYH59kK/QV11Hh
3lTC5ZH7obu6tftC6HHPym859ZKxYVXRSwEng1R91BiCkUyr2jmCHkvj6hqH6YiB
7MN5mZcqtM9FRt3ZnVYT6BWtm9vMF6IuxBjj3uuPMMnmQEC8ont8NZ8LRN2HW54U
BD3nNm7fDVZw5R45WWztUIZkJO/rPsIoRw2m4EsWkDtxXDWI3fHTh+yXYIAQnIns
s72yiaLOOyi9t7FtXzFm07J3B5AlqhFA+nsPUHOOUL/35d4iTl2EZ0mGQ6EWhjgz
/GtjQvH7P57yBeZGPuT+342JvGAG79FVBgZVr1lv8LQRa0F8TNwP0TAVo1PlKYVl
lgqdTzAzdkkzh48kMSy4Hkxcyy/bLPuwhkKbIZEUQyyDrM1eQ6k=
=X8m/
-----END PGP SIGNATURE-----