[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Jesper Cockx]

On Wed, Jan 8, 2014 at 9:41 PM, Conor McBride <conor at strictlypositive.org>wrote:

>
> One reason why my brief career as a singer-songwriter was curtailed is that
> I could never remember the words, but I think it highly unlikely that the
> paper we wrote back then made any kind of assurance about mutual
> definitions
> like moo and noo. If I did, then perhaps I join the good company in error,
> for which I apologize.
>

I'm sorry, I meant the version of noo I gave in my previous mail. I'd
better call it something else:

woo : (X : Set) -> (WOne <-> X) -> X -> Zero
woo .WOne Refl (wrap f) = woo (Zero -> WOne) myIso f

bad : Zero
bad = woo WOne Refl (wrap \ ())

The definition of woo falls within the framework of EDPM. Moreover, it is
structurally recursive on its third argument. It is still incompatible with
univalence (as shown by 'bad'), and it cannot be translated to eliminators.


> I quite agree that the definition of "structurally smaller" we gave does
> say
> that
>
>   f < wrap f
>
> where f amounts to a collections of (no) things, all of which are smaller
> than (wrap f). NOWHERE is it said that transporting f with respect to an
> equation on types respects structural ordering relations, and ESPECIALLY
> IN THE PRESENCE OF UNIVALENCE that is OBVIOUS NONSENSE.
>

Of course, transporting a term along an equation should not preserve
structural ordering. Yet we should still be able to pattern match on
equality proofs (in the --without-K sense), as long as the definition can
be translated to eliminators.


> Eliminators are ok because they fix the "view" of the datatype for the
> whole of the recursion. They don't allow you to make up spurious,
> allegedly smaller, elements of the type by shipping stuff across
> isomorphisms.
>

I agree, and I think neither should pattern matching let us do this (at
least not with --without-K enabled). But wasn't the whole point of EDPM to
show that it *is* safe to use pattern matching? What Daniel and Thomas on
the Coq list showed, is that we need an additional criterion for pattern
matching to be safe. My proposal is to require that the type of the
argument on which the function is structurally recursive, should be a data
type. A different (and probably much more sophisticated) proposal was given
on the Coq list. Do you have another proposal?

On the long term, I think the best way to go would be to actually perform
the translation of pattern matching to eliminators in Agda, similar to
Matthieu's Equations plugin for Coq. There are just too many subtleties to
pattern matching to get everything correct otherwise, especially when
univalence and higher inductives are involved.

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