This is related to a previous discussion on this mailing list : https://groups.google.com/d/msg/homotopytypetheory/b96TBt0Bn7Y/Ii= AcnUL2AQAJ, "What is known and/or written about =E2=80=9CFrobenius eliminators=E2=80=9D?".

I noticed recently that the Frobenius eliminator for identity types is related to the notion of strong logical equivalence (the trivial fibrations of the left semi-model structure on the category of CwAs with Sigma and Id introduced in https://arxiv.org/abs/161= 0.00037,"The homotopy theory of type theories").

The Frobenius, Paulin-Mohring variant of the J eliminator is presented by the following inference rule:
=C2=A0 G |- A type =C2=A0 G |- x : A
=C2=A0 G, y:A, p:Id(x,y) |- B(y,p) type*
=C2=A0 G, y:A, p:Id(x,y), b:B(y,p) |- C(y,p,b) type
=C2=A0 G, b:B(x,refl(x)) |- c : C(x,refl(x),b) type
=C2=A0 G |- y : A=C2=A0=C2=A0=C2=A0 G |- p : Id(x,y)=C2=A0=C2=A0=C2= =A0 G |- b:B(y,p)
--------------------------------------------------------
=C2=A0 G |- J(A,x,B,C,c,y,p,b) : C(y,p,b)

(where "B(y,p) type*" means that B(y,p) is a finite sequence of types over "G, y:A, p:Id(x,y)", i.e. a context in the contextual slice over "G, y:A, p:Id(x,y)")

(In the discussion linked above, Valery Isaev gives a proof that if the type theory includes sigma types, the "simple" Paulin-Mohring eliminator is strong enough to derive the "Frobenius" variant. This is also proven by Paige Randall North in https://arxiv.org/abs/190= 1.03567, in a more categorical setting.)

I consider roughly the same framework as in "The homotopy theory of type theories".

Recall that a contextual morphism F : C --> D is a strong logical equivalence if it satisfies term lifting and type lifting conditions:
- type lifting: for every context G in C, F_G : Ty_C(G) -> Ty_D(F(G)) is surjective.
- term lifting: for every context G in C and type A over G, F_A : Ter_C(G,A) -> Ter_D(F(G),F(A)) is surjective.

Let C be a CwA with Id and refl. The J eliminator for some pointed type (A,x) in some context G can be seen as the statement that the contextual morphism F : C[G,y:A,p:Id(x,y)] --> C[G] (where C[G] is a notation for the contextual slice over G), sending (y,p) to (x,refl(x)), satisfies the term lifting condition. Indeed, the input of the term lifting condition is the data of B, C and c, and the output is a term J in the context G,y:A,p:Id(x,y),b:B(y,p) of type C(y,p,b), such that F(J) =3D c.

The type lifting condition can then be derived, assuming that C does not include weird type equalities (for instance, when C is cofibrant/freely generated, or when C is equipped with a hierarchy of universes ensuring that every type belongs to a unique universe).

If we only require F to be a weak logical equivalence (a weak equivalence in the left semi-model structure), then we obtain propositional identity types. I think that asking for F to be an isomorphism forces the identity types to become extensional.

Has this been studied before ? Can this be extended to the elimination rules of other type formers ?

Best regards,
Rafa=C3=ABl Bocquet

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/a20122bc-289b-4fce-1183-76b66aed395f%40ens.fr.