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
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
- 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
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 ?