[Agda] Fin n -> Fin n extensional?

Mon Feb 23 19:50:43 CET 2015

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:
> -----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-----
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda