[Agda] Re: Yet another way Agda --without-K is incompatible with univalence

[Jesper Cockx]

Matteo,

PS. I still do not understand why by using a parameterised module the
> file is not accepted, as that is the way I most often assume
> "postulates" and I thought the outcome would be the same. However, I
> admit I do *not* understand the details of the problem.
>

I think the reason why your version with the parametrized module is not
accepted, is that Agda treats data types inside a parametrized module as
parametrized data types. I.e. the definition of Foo in your version your
version is equivalent with

 data Foo (mySpace : Set) (myPoint : mySpace) : myPoint ≡ myPoint → Set
where
  foo : Foo refl

For parametrized data types, the current --without-K implementation
performs parameter reconstruction (as implemented by Nils). I.e. for the
purpose of checking --without-K, the constructor foo is considered to have
type "(mySpace : Set) (myPoint : mySpace) -> Foo refl". Now we cannot
eliminate the argument of type "foo mySpace myPoint ≡ foo mySpace myPoint"
because the variables mySpace and myPoint are not used linearly.

In contrast, in my example there are no parameters (of the module or the
data kind), so parameter reconstruction does not help. In fact, you can
replace my postulates of mySpace and myPoint by any concrete values (for
example a sphere) as long as they do not contain parameters or free
variables, and the file still typechecks. This is clearly not what we want.

Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140117/235efdfd/attachment.html