Frobenius eliminators

[Rafaël Bocquet]

This is related to a previous discussion on this mailing list : https://groups.google.com/d/msg/homotopytypetheory/b96TBt0Bn7Y/IiAcnUL2AQAJ, "What is known and/or written about “Frobenius eliminators”?".

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/1610.00037,"The homotopy theory of type theories").

The Frobenius, Paulin-Mohring variant of the J eliminator is presented by the following inference rule:
  G |- A type   G |- x : A
  G, y:A, p:Id(x,y) |- B(y,p) type*
  G, y:A, p:Id(x,y), b:B(y,p) |- C(y,p,b) type
  G, b:B(x,refl(x)) |- c : C(x,refl(x),b) type
  G |- y : A    G |- p : Id(x,y)    G |- b:B(y,p)
--------------------------------------------------------
  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/1901.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) = 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ël Bocquet