Safe propositional resizing in Agda

[Martin Escardo]

Vladimir gave a talk about resizing axioms in Bergen at the Types
meeting in 2011 in a plenary lecture:


https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2011_Bergen.pdf

As I understand, in UniMath this is achieved by working with Type:Type.
(But this may have evolved to a safer incarnation since I checked it.)

Agda now has a new "--rewriting" option that allows one to postulate
constants with computational behaviour specified by rewrite rules:

Jesper Cockx and Andreas Abel.
Sprinkles of extensionality for your vanilla type theory,
Types 2016, Novi Sad, Serbia, 23-26 May 2016.
http://www.types2016.uns.ac.rs/index.php/programme-2/conf-prog

https://people.cs.kuleuven.be/~jesper.cockx/rewrite-rules/sprinkles-of-extensionality.pdf

Using this, it is possible to implement propositional resizing in Agda
without Type:Type:

http://www.cs.bham.ac.uk/~mhe/impredicativity-via-rewriting/

This is supposed to be safe: the rewriting is confined to just one short
module, prop.agda, to make the type Prop := Sigma(P:U0).isProp P to live
in U0 rather than U1. (Or at least as safe as propositional resizing
itself is in theory.)

Details of how this works can be found in the extensive comments
provided in the above (relatively short) development.

Currently this works only with the stable development version 2.5.2 of
Agda, for reasons explained in the file resize.agda, while the released
version of Agda is 2.5.1. Get stable 2.5.2 with

$ git clone https://github.com/agda/agda -b stable-2.5
$ cd agda
$ cabal install

Thanks to Jesper and Andreas.

Martin
PS. I wonder if --rewriting can be used to get cubicaltt in Agda.