[Agda] Fin n -> Fin n extensional?

[Neelakantan Krishnaswami]

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

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
> 
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.14 (GNU/Linux)

iQIbBAEBAgAGBQJU60laAAoJEFHmop5RZGmSfJcP91HMj9P8+iiF344OtyF+Pfv1
IUk+w4IndUMQcDPFys0GCX9VyMeg5W3ezwV1eYYLNlSghtR/rWAVtKRlDH/PQ8Hp
Q9RJhpEo3gNMW1cBSHWTM7HpmcI2z8ttualtE/1+yK4XPRC0vXw6V6mOHv4KmDES
xjhsKy4ut8Ah4pTXvb0+MkTvI46F7dpBlkpQmAFygpfOtNz7ahZ4+bQjlmdPMu6B
DG9jwtA9HuEBoxR84Fni0w9gA5da+Ew7cF0mcuG777RK3M6NnuB+jnyk18w7qUKv
bQ9s4Is0YZ4KHkDmNe6tVnTbDaivzQfN6rBTFPfrRPHCo0b4cU3Dpos7dQdOf56a
qvlmC8hoB60KGaLYx+SqjAHfEudHsTPzpDQUHZE0T+zlqLBI1g8y9my20rd5PN3t
S4sapKOVsVibd+XnNbGDhoRDA4Uy1KccO0O9Yt8w1/yTpJqik4DfB8g7tEIzsgc+
137F+WnUfNiilpukOWrhzSRmxpmOgGZaA96o4tsq6eZjf8w9OSZeYFzEqn+pCtci
gClqrFGIdbBXHEcOMnJ5K+Y1y+1himsvfM8XavdE0tTfv2+aGknpwm9qRs6SG7+w
gNV18wNhkL6BqdDTnEIJ6y1PvK/IDmi6D9Ar9eL8nvcELzzsEbDFLFWkm/ElSzZ6
OC285Dst5uKeClsp238=
=qT5j
-----END PGP SIGNATURE-----