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.