[Agda] Are there unicorns in Agda?

[Gabriel Scherer]

> At the moment it seems that there will be unicorns in such a model

And rightly so, I would say : maybe the possibility to be consistently
extended with unicorns is one of the strenghts of MLTT?

The specificity of the unicorn case (with respect to Set -> Set which
is perfectly correct) is the downsizing, which in this case (type to
term) would break parametricity, as Dan noted.

However, I don't think we can expect parametricity to hold in all
Martin-Löf style calculi. Parametricity is essential for impredicative
calculus starting as System F, as breaking it will usually make the
logic inconsistent; see Harper's "Parametricity and variants of
Girard's J operator" which uses a `TypeEq : Set → Set → Two`
type-equality predicate to build a non-normalizing term. I'm not sure
you could build such a term from any unicorn (though unicorns may be
considered conjunctions of partial applications of TypeEq), but that
would prove that consistent impredicative calculi don't have them.

Predicative theories however are more resilient to
non-parametricity. I think that there could be perfectly reasonable
Martin-Löf-style theories with unicorns. For example, consider the
"explicit" presentations of universes, with a type of "type codes" and
an `El` operator in the type world.
  U₀ type
  a : U₀ ⊢ (El a) type

  poly_id : (a : U₀) → (x : El a) → El a

In this setting, types are reified into codes at the term level, and
polymorphic functions have access to the type-code directly. It seems
perfectly natural to allow some non-parametric operations on type
codes — a destructor on U₀ – and, if I'm correct, that's what people
do when the define a deep embedding of a simpler dependent type theory
into Agda.

This is hand-waving, so I may very well be wrong – indeed "perfectly
natural" extensions often break consistency — but I think you can't
exclude unicorns from general Martin-Löf theories. The property of not
having unicorns is not stable by extension of the calculus, so it's
only true of conveniently restricted theories which respect
parametricity and allow type-erasure.



On Fri, Nov 11, 2011 at 4:35 PM, Martin Escardo <m.escardo at cs.bham.ac.uk> wrote:
>
>
> On 11/11/11 15:15, Andreas Abel wrote:
>>
>> I welcome your research
>> which would give more precise models.
>
> At the moment it seems that there will be unicorns in such a model, although
> not necessarily boolean valued.
>
> This is the reason I wrote the question.
>
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>