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

[Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>]

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

On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <valery.isaev@gmail.com> 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 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?

–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.
For more options, visit https://groups.google.com/d/optout.

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