Looking for counterexample

[Altenkirch Thorsten]

When formulating the eliminator for equality in the absence of Pi-types we need to generalize it (this is related to the Frobenius condition):

We say

G,x,y:A,p:x=y,D |- P

G,x:A,D[y=x,p=refl] |- m : P[y=x,p=refl] 

------------------------------------------------------

G,,x,y:A,p:x=y,D |- J(m) : P

and the first example where we need this is when we want to prove transitivity,

G,x,y,p:x=y,(z:A,q:y = z) |- J(q) : x=z

Moreover there doesn't seem to be a way to avoid this. I cannot do induction over q because I would need to move the y over the p.

However, when using the Paulin-Mohring eliminator we don't need D in this case

G |- a : A

G,y:A,p:a=y |- P

G |- m : P[y=x,p=refl]

----------------------------------

G,y:A,p:a=y |- J'(a,m) : P

G,x,y,p:x=y,z:A,q:y = z |- J'(y,q) : x=z

With the PM eliminator the need for D disappears because I can just eliminate over q. I also looked at some other examples (associativity for transitivity, functoriality of transitivity and couldn't find an example where the simple rule wouldn't be sufficient.

Is this true in general (the PM rule without the D is sufficient)? Or is there a counterexample to that conjecture?

Thorsten

[Guillaume Brunerie]

I think that you need the D to define transport.

On the other hand you don’t need the D to define the infinity-groupoid
structure on any type and the infinity-functor structure on any
function (because by definition the contractible contexts can be
contracted by induction on the last term of the context).

Guillaume

2013/4/14 Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk>:

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>

[Altenkirch Thorsten]

On 14/04/2013 18:08, "Guillaume Brunerie" <guillaume...@gmail.com>
wrote:

>I think that you need the D to define transport.

I thought transport just is J' when P doesn't depend on the proof?

>On the other hand you don¹t need the D to define the infinity-groupoid
>structure on any type and the infinity-functor structure on any
>function (because by definition the contractible contexts can be
>contracted by induction on the last term of the context).

Yes, indeed - this is a good point.

Moreover, this would still work if we allowed the more general definition
of contractible (where the first reference doesn't need to be a variable).

Thorsten

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

[Guillaume Brunerie]

On 2013/4/14 Altenkirch Thorsten <psz...@exmail.nottingham.ac.uk> wrote:
> On 14/04/2013 18:08, "Guillaume Brunerie" <guillaume...@gmail.com>
> wrote:
>
>>I think that you need the D to define transport.
>
> I thought transport just is J' when P doesn't depend on the proof?

Hmm, I was thinking of the following:

G, x:A, y:A, p:x=y, u:P(x) |- transport P p u : P(y)

>>On the other hand you don¹t need the D to define the infinity-groupoid
>>structure on any type and the infinity-functor structure on any
>>function (because by definition the contractible contexts can be
>>contracted by induction on the last term of the context).
>
> Yes, indeed - this is a good point.
>
> Moreover, this would still work if we allowed the more general definition
> of contractible (where the first reference doesn't need to be a variable).

Yes, it would be quite natural to do that (at least from this point of view).

Guillaume