[Agda] Are there unicorns in Agda?

[Peter Hancock]

On 11/11/2011 01:13, Martin Escardo wrote:
> I would like to know whether there are unicorns in Martin-Lof type
> theory with universes. By a universe I don't mean an inductively
> defined gadget, but simply something like Set in Agda.
>
> A unicorn is a map F : Set → Two, where Two is the two-element set,
> such that there are sets X and Y with F X ≠ F Y.

I shudder to think what you might call them (nrocinus?), but instead of functions
*on* Set which have data values, you could consider functions *to* Set
(or other large type) which have data-arguments.  Both Jan Smith and
Daniel Fridlender have constructed models of Martin-Lof type theory (without
any universe which is a set, eg the Boolean universe) in which all set-valued functions (predicates)
on a set are constant. The predicates you can define do not discriminate between
any data items.

This is quite interesting I think for pointing to the need of some kind of principle
for large elimination, or large-valued induction-recursion.  Without it, type-theory
seems to be woefully inexpressive.

Hank

By the way, unicorns seem to be related to the "Uniformity Principle" that was
studied by Troelstra and others in the 1970's.  It is consistent with HA2, ie
Heyting arithmetic with impredicative predicate/proposition quantification.