[Agda] Fin n -> Fin n extensional?

Tue Feb 24 10:45:29 CET 2015

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hello,

This is a good point.

However, you can retain a type preserving definitional equality
validating K, even without eta-expanding identity proofs, simply
by equating all terms at identity type:

Γ ⊢ q : Id[X](e,e')
Γ ⊢ p : Id[X](e,e')
————————————————————————
Γ ⊢ p ≡ q : Id[X](e,e')

A type-directed equality algorithm will hit the Id case and then
stop with success. You can do the same for units and empty types,
even if you view them as positive types.

If you know the type is a subsingleton, then definitional equality can
always succeed. In the case of Id, this rule *makes* it into a
subsingleton, of course! (Or rather, ensures that the syntax can only
be interpreted by models in which equality is a subsingleton -- which
rules out univalent models.)

Best,
Neel

On 23/02/15 22:29, Andrea Vezzosi wrote:
> Jon,
> 
> Yeah, I was going to add that eta expanding Id[X](e,e') to refl is 
> only type preserving when e and e' are judgementally equal, and in
> an open context they might not be.
> 
> Best, Andrea
> 
> On Mon, Feb 23, 2015 at 9:05 PM, Jon Sterling
> <jon at jonmsterling.com> wrote:
>> Andrea,
>> 
>> Out of curiosity, is the reason that Agda does not do eta
>> expansion at the identity type because it would cause false
>> identifications to become true judgementally in an open term?
>> 
>> Kind regards, Jon
>> 
>> 
>> On Mon, Feb 23, 2015, at 10:50 AM, Andrea Vezzosi wrote:
>>> As a side note, Agda doesn't actually do any eta expansion at
>>> the Id type, e.g. two postulated equalities won't be
>>> judgementally equal.
>>> 
>>> However without postulates (or primTrustMe) it is still the
>>> case that every proof of equality in a closed context will
>>> evaluate to refl. Axiom K actually computes away as soon as the
>>> proof becomes refl, so it's not making this any harder.
>>> 
>>> 
>>> Cheers, Andrea
>>> 
>>> On Mon, Feb 23, 2015 at 4:38 PM, Neelakantan Krishnaswami 
>>> <n.krishnaswami at cs.bham.ac.uk> wrote:
> Hello,
> 
> Definitional equality including Axiom K (uniqueness of identity
> proofs) remains decidable.
> 
> The reason is that you can split the implementation of judgemental 
> into two alternating phases -- weak-head normalization and 
> type-directed eta-expansion. Just as with eta for unit, this means 
> that when you compare terms at equality type, you can simply
> succeed.
> 
> Concretely, if you have proofs p and q at type Id[X](e,e') such
> that p,q :  Id[X](e,e'), then you can eta-expand to p ==> refl and 
> q ==> refl, and then refl will be judged to be equal to itself.
> 
> If you restrict "computation" to mean beta-reduction, then
> equality proofs do not all have to *reduce* to refl. However, they
> all can *eta-expand* to refl.
> 
> IMO, a very good reference on this is Andreas Abel's habilitation 
> thesis. If you're in a hurry, then his FOSSACS 2011 paper with
> Gabriel Scherer "On Irrelevance and Algorithmic Equality in
> Predicative Type Theory" was a relatively accessible introduction
> to this approach.
> 
> 
> Best, Neel
> 
> On 19/02/15 20:54, Abhishek Anand wrote:
>>>>>> Thanks Jason. Your argument is convincing. Already at the
>>>>>> second line,  (\_ → 0) and (\_ → 1)  being definitionally
>>>>>> equal contradicts my understanding of Coq's definitional
>>>>>> equality. Are your assumptions valid in Agda with K? In
>>>>>> other words, is it true that in Agda with K, any proof of
>>>>>> equality (Id) of closed terms computes down to refl?
>>>>>> 
>>>>>> 
>>>>>> Thanks, -- Abhishek http://www.cs.cornell.edu/~aa755/
>>>>>> 
>>>>>> On Wed, Feb 18, 2015 at 12:06 PM, Jason Gross 
>>>>>> <jasongross9 at gmail.com> wrote:
>>>>>> 
>>>>>>> Here's one, I think, for showing impossibility of
>>>>>>> inhabiting the type (f g : Void → ℕ) → Id f g: Assuming
>>>>>>> the type theory is strongly normalizing on terms of
>>>>>>> identity type, the only closed proof of equality of two
>>>>>>> closed functions must be refl.  Thus, if (\_ → 0) and
>>>>>>> (\_ → 1) are equal, they must be definitionally equal
>>>>>>> in a strongly normalizing type theory.  From (Id f g),
>>>>>>> we can obtain (x : Void) → Id (f x) (g x); it's
>>>>>>> behavior is to send refl to refl.  Thus, when we plug
>>>>>>> in refl : Id (\_ → 0) (\_ → 1), we get a proof of Void
>>>>>>> → Id 0 1 which reduces to \_ → refl.  But this is a
>>>>>>> contradiction, for refl does not prove Id 0 1.
>>>>>>> 
>>>>>>> On Wed, Feb 18, 2015 at 11:37 AM, Abhishek Anand < 
>>>>>>> abhishek.anand.iitg at gmail.com> wrote:
>>>>>>> 
>>>>>>>> Unprovability of void-ext has been known to be the
>>>>>>>> reason why one cannot (in Coq) code up natural
>>>>>>>> numbers as W Types.
>>>>>>>> 
>>>>>>>> Here is a quote : "This is because one cannot prove
>>>>>>>> that there is only a unique function from the empty
>>>>>>>> set to the set of natural numbers without using
>>>>>>>> extensional equality." from 
>>>>>>>> https://coq.inria.fr/cocorico/WTypeInsteadOfInductiveTypes
>>>>>>>>
>>>>>>>>
>>>>>>>> 
However, I don't know a formal (meta-theoretical) proof of
>>>>>>>> unprovability of void-ext. I'd be grateful if someone
>>>>>>>> can point us to such a  proof.
>>>>>>>> 
>>>>>>>> 
>>>>>>>> -- Abhishek http://www.cs.cornell.edu/~aa755/
>>>>>>>> 
>>>>>>>> On Wed, Feb 18, 2015 at 11:20 AM, Dan Licata
>>>>>>>> <drl at cs.cmu.edu> wrote:
>>>>>>>> 
>>>>>>>>> Can you even do this (without otherwise assuming
>>>>>>>>> function extensionality)?
>>>>>>>>> 
>>>>>>>>> For example, for Fin 0, isn't it the same as saying
>>>>>>>>> "any function from 0 to A is abort":
>>>>>>>>> 
>>>>>>>>> data Id {A : Set} (a : A) : A → Set where refl : Id
>>>>>>>>> a a
>>>>>>>>> 
>>>>>>>>> data Void : Set where
>>>>>>>>> 
>>>>>>>>> abort : {A : Set} → Void → A abort ()
>>>>>>>>> 
>>>>>>>>> void-ext : {A : Set} → (f : Void → A) → Id f abort
>>>>>>>>> void-ext f = {!!}
>>>>>>>>> 
>>>>>>>>> (void-ext is sufficient; is it necessary?) and if
>>>>>>>>> so, can you prove that?  I don't see how off the
>>>>>>>>> top of my head.
>>>>>>>>> 
>>>>>>>>> -Dan
>>>>>>>>> 
>>>>>>>>> On Feb 18, 2015, at 10:47 AM, João Paulo Pizani
>>>>>>>>> Flor < J.P.PizaniFlor at uu.nl> wrote:
>>>>>>>>> 
>>>>>>>>> Not yet (couldn't find it anywhere), but I will
>>>>>>>>> probably need it for my Ph.D project, so maybe it
>>>>>>>>> will come in some time...
>>>>>>>>> 
>>>>>>>>> Cheers,
>>>>>>>>> 
>>>>>>>>> João Pizani, M.Sc <j.p.pizaniflor at uu.nl>
>>>>>>>>> Promovendus - Departement Informatica Faculteit
>>>>>>>>> Bètawetenschappen - Universiteit Utrecht
>>>>>>>>> 
>>>>>>>>> On Wed, Feb 18, 2015 at 3:25 PM, Jacques Carette 
>>>>>>>>> <carette at mcmaster.ca> wrote:
>>>>>>>>> 
>>>>>>>>>> Does anyone have a proof in Agda that functions
>>>>>>>>>> at type (Fin n -> Fin n) are extensional?
>>>>>>>>>> Jacques 
>>>>>>>>>> _______________________________________________
>>>>>>>>>> Agda mailing list Agda at lists.chalmers.se 
>>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> _______________________________________________
>>>>>>>>> Agda mailing list Agda at lists.chalmers.se 
>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>>> _______________________________________________
>>>>>>>>> Agda mailing list Agda at lists.chalmers.se 
>>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>>> 
>>>>>>>>> 
>>>>>>>> 
>>>>>>>> _______________________________________________ Agda
>>>>>>>> mailing list Agda at lists.chalmers.se 
>>>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>>>> 
>>>>>>>> 
>>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> 
>>>>>> _______________________________________________ Agda
>>>>>> mailing list Agda at lists.chalmers.se 
>>>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>>> 
>>>> _______________________________________________ Agda mailing
>>>> list Agda at lists.chalmers.se 
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>> _______________________________________________ Agda mailing
>>> list Agda at lists.chalmers.se 
>>> https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________ Agda mailing
>> list Agda at lists.chalmers.se 
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________ Agda mailing list 
> Agda at lists.chalmers.se 
> https://lists.chalmers.se/mailman/listinfo/agda
> 
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.14 (GNU/Linux)

iQIcBAEBAgAGBQJU7Eg5AAoJEFHmop5RZGmSND8QAIYdzpshHhbvJdCToFTHlysE
Yqjeb7kgYk3kaYtQsrVSbe51srfSDrxUCT+WoQS3dpXsduXup+pa5XWDX6rQ5SY8
T7Xd2pLOEDF/lkjDvGtZd1RHFa/tYA3IkyZkxPisQroEWEH8JWMz1B0uedwZx23y
c3cCaSpSd8mNX2IemcH+FtGLngp/mez7V09YUR/J9ETRsmgyl1u7iJRNW018FB36
qhtk4P0Sg/2C+13yLLJkkBy55X6iS3wQAJwLo3FXxJy2rBZJUcEt3R+da2LU3bBS
8q2EMTf5NOJBIFwOUWWgZMkyh4lyAaiiKPFwUKjQ2S0Nofkb/49YdSGw4vpuR1+u
HxXDagO+8wZNn5PC/nDhbZFUhoc7raq3ADd3ft8HStedLVZvnVUun/EK+ZOzubGy
YogUVoPZTmnl2PC/oSmrRvUsoPn4eLh9JYrrdbDUVtr4U8V8IPedoOmvJ7gDe0FI
TXDA7PpSgoLFog+YhuNVow8QNyrBA00SSE7iqYwbi7UhQ+8flomOB3dhJncG1OzM
EEfXCu6S2oe4ekYYDhM/2RHW7Q+No7HmKowqjLnlsoxKGJC5jjVrU7sGl/2qKVTQ
V9r9MOdfzqZOv0TCGHApcpYttILiEtcel2OiUF3eFo6cVaDa/NK2SKeeil2RdHbT
9EvbHgX7FRCYtTqxlMeq
=Csvc
-----END PGP SIGNATURE-----