Re: [HoTT] What is known and/or written about “Frobenius eliminators”?

["Rafaël Bocquet" <rafael.bocquet@ens.fr>]

[-- Attachment #1: Type: text/plain, Size: 5017 bytes --]

Hi,

Here's a simple countermodel that shows that the Martin-Löf eliminator 
(two-sided eliminator) for identity types is not strong enough to derive 
transport in the absence of Pi-types.

Consider the initial model of a type theory with Id, refl, a closed type 
A, a type family B over A, and closed terms x,y : A, b : B x and p : 
Id_A x y.

It can be shown that the only terms of that model are the variables, the 
weakenings of the generators and their iterated refls.

Because there is no closed term of type B y, transport does not hold in 
this model.

However, unless I missed some cases, it is still possible to define the 
Martin-Löf eliminator by case distinction on the elimination target.

Best,
Rafaël

On 3/23/20 10:54 AM, Ambrus Kaposi wrote:
> Hi,
>
> Sorry for resurrecting an old thread, I just wanted to document that 
> Frobenius J can be derived from Paulin-Mohring J without Pi, Sigma or 
> universes: 
> https://github.com/akaposi/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda
> This was observed by Rafael Bocquet and András Kovács in October 2019, 
> but maybe other people have known about this.
>
> We mention this briefly in our paper on HIIT signatures where 
> Paulin-Mohring J can be used on previous equality constructors but we 
> don't have Pi, Sigma or (usual) universes: 
> https://lmcs.episciences.org/6100
>
> Cheers,
> Ambrus
>
> 2018. július 13., péntek 13:05:47 UTC+2 időpontban Valery Isaev a 
> következőt írta:
>
>
>     2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine
>     <p.l.l...@gmail.com <javascript:>>:
>
>         On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev
>         <valer...@gmail.com <javascript:>> wrote:
>
>             Hi Peter,
>
>             I've been thinking about such eliminators lately too. It
>             seems that they are derivable from ordinary eliminator for
>             most type-theoretic constructions as long as we have
>             identity types and sigma types.
>
>
>         Thankyou — very nice observation, and (at least to me) quite
>         surprising!
>
>
>     I was surprised too. The case of coproducts is especially unexpected.
>
>             I mean a strong version of Id:
>
>
>         Side note: this is I think more widely known as the
>         Paulin-Mohring or one-sided eliminator for Id-types; the HoTT
>         book calls it based path-induction.
>
>                 The fact that the Frobenius version is strictly
>                 stronger is known in folklore, but not written up
>                 anywhere I know of. One way to show this is to take
>                 any non right proper model category (e.g. the model
>                 structure for quasi-categories on simplicial sets),
>                 and take the model of given by its (TC,F) wfs; this
>                 will model the simple version of Id-types but not the
>                 Frobenius version.
>
>             Are you sure this is true? It seems that we can interpret
>             the strong version of J even in non right proper model
>             categories. Then the argument I gave above shows that the
>             Frobenius version is also definable.
>
>
>         Ah, yes — there was a mistake in the argument I had in mind. 
>         In that case, do we really know for sure that the Frobenius
>         versions are really strictly stronger?
>
>     I don't know how to prove this, but it seems that we can't even
>     define transport without Frobenius J. Also, if we do have
>     transport and we know that types of the form \Sigma (x : A)
>     Id(a,x) are contractible, then the "one-sided J" is definable, so
>     if we want to prove that the Frobenius version does not follows
>     from the non-Frobenius, we need to find a model where either
>     transport is not definable or \Sigma (x : A) Id(a,x) is not
>     contractible.
>
>         –p.
>
>
>
> -- 
> You received this message because you are subscribed to the Google 
> Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.com 
> <mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/ade5cab1-5df2-41c9-b412-ac561fbe77bc%40googlegroups.com 
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/ade5cab1-5df2-41c9-b412-ac561fbe77bc%40googlegroups.com?utm_medium=email&utm_source=footer>.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/17a9e7e7-e03b-cf03-58de-5f1f77d74469%40ens.fr.

[-- Attachment #2: Type: text/html, Size: 12088 bytes --]