[Agda] Are there unicorns in Agda?

[Martin Escardo]

Interesting remarks, Hank.

One possible reaction to the result I presented is that Rice's Theorem 
for the universe is to be expected: after all, there are no elimination 
rules for the universe, and so how could one possibly define any 
function out of Set? But the arguments I gave show that, even if there 
were elimination rules, Rice's Theorem for the universe would still 
hold, which justifies the lack of elimination rules. (For instance, it 
follows that pattern matching in Set cannot be used to define 
extensional functions on Set, and, indeed, such definitions by pattern 
matching in Set necessarily break extensionality.) The argument I gave 
doesn't use syntax or models. It is just a theorem of ML type theory.

Best,
Martin

On 11/02/12 20:22, Peter Hancock wrote:
> 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.
>
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe