[Agda] Fin n -> Fin n extensional?

[Peter Selinger]

This discussion reminds me that I have basically very little idea what
equality of functions means in Agda. It may be one of the places where
Agda differs from Coq. Unfortunately, the reference manual is mostly
silent on this point, except for an obscure reference on the page on
functions:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Functions

In the subsection on pattern matching lambdas, the manual states that
"pattern matching functions are generative. For instance, refl will
not be accepted as an inhabitant of the type

  (λ { true → true ; false → false }) ≡
  (λ { true → true ; false → false }),

because this is equivalent to extlam1 ≡ extlam2 for some distinct
fresh names extlam1 and extlam2."

>From this, I inferred that function equality in Agda is definitional
equality, i.e., two functions are equal if and only if they are
internally represented as pointers to the same closure. 

However, this does not seem to be the case in general. For most
functions, Agda seems quite happy to accept refl as an inhabitant as
long as the two functions are beta-eta equivalent. For example,

test : {a : Set} -> (λ(x : a -> a) -> λ(y : a) -> x y) ≡ (λ(x : a -> a) -> x)
test = refl

Apparently it is only for pattern-matching functions that definitional
equality is used. So the correct answer for most purposes seems to be:
Agda equality at function types is a random, but fixed, relation that
is contained in beta-eta equality and that contains definitional
equality.

In particular, one cannot prove extensionality for any function whose
domain is a datatype (such as Void or Fin n), because one can just
write down two identical copies of some pattern-matching function, and
they won't be equal.

-- Peter

Abhishek Anand 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