Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] What is known and/or written about “Frobenius eliminators”?
@ 2018-07-12 15:15 Peter LeFanu Lumsdaine
  2018-07-12 17:06 ` Valery Isaev
                   ` (2 more replies)
  0 siblings, 3 replies; 9+ messages in thread
From: Peter LeFanu Lumsdaine @ 2018-07-12 15:15 UTC (permalink / raw)
  To: HomotopyTypeTheory@googlegroups.com

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

Briefly: I’m looking for background on the “Frobenius version” of
elimination rules for inductive types.  I’m aware of a few pieces of work
mentioning this for identity types, and nothing at all for other inductive
types.  I’d be grateful to hear if anyone else can point me to anything
I’ve missed in the literature — even just to a reference that lays out the
Frobenius versions of the rules for anything beyond Id-types.  The
proximate motivation is just that I want to use these versions in a paper,
and it’d be very nice to have a reference rather than cluttering up the
paper by writing them all out in full…

In more detail: Here are two versions of the eliminator for identity types:

Γ, x,y:A, u:Id(x,y)  |– C(x,y,u) type
Γ, x:A |– d(x) : C(x,x,r(x)) type
Γ |— a, b : A
Γ |— p : Id(a,b)
——————————————
Γ |— J(A, (x,y,u)C, (x)d, a, b, p) : C(a,b,p)

Γ, x,y:A, u:Id(x,y), w:Δ(x,y,u) |– C(x,y,u,w) type
Γ, x:A, w:Δ(x,x,r(x)) |– d(x,w) : C(x,x,r(x),w) type
Γ |— a, b : A
Γ |— p : Id(a,b)
Γ |— c : Δ(a,b,p)
——————————————
Γ |— J(A, (x,y,u)Δ, (x,y,u,w)C, (x,w)d, a, b, p, c) : C(a,b,p,c)

(where Δ(x,y,u) represents a “context extension”, i.e. some finite sequence
of variables and types w_1 : B_1(x,y,u), w_2 : B_2(x,y,u,w_1), …)

I’ll call these the “simple version” and the “Frobenius version” of the
Id-elim rule; I’ll call Δ the “Frobenius context”.  The simple version is a
special case of the Frobenius one; conversely, in the presence of Pi-types,
the Frobenius version is derivable from the simple one.

Most presentations just give the simple version.  The first mention of the
Frobenius version I know of is in [Gambino, Garner 2008]; the connection
with categorical Frobenius conditions is made in [van den Berg, Garner
2008], and some further helpful explanatory pointers are given in [Gambino,
Sattler 2015].  It’s based on this that I use “Frobenius” to refer to these
versions; I’m open to suggestions of better terminology.  (All references
are linked below.)

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.

Overall, I think the consensus among everyone who’s thought about this
(starting from [Gambino, Garner 2008], as far as I know) is that if one’s
studying Id-types in the absence of Pi-types, then one needs to use the
Frobenius version.

One can also of course write Frobenius versions of the eliminators for
other inductive types — eg Sigma-types, W-types, …  However, I don’t know
anywhere that even mentions these versions!

I remember believing at some point that at least for Sigma-types, the
Frobenius version is in fact derivable from the simple version (without
assuming Pi-types or any other type formers), which would explain why
no-one’s bothered considering it… but if that’s the case, it’s eluding me
now.  On the other hand, I also can’t think of a countermodel showing the
Frobenius version is strictly stronger — wfs models won’t do for this,
since they have strong Sigma-types given by composition of fibrations.

So as far as I can see, if one’s studying Sigma-types in the absence of
Pi-types, one again might want the Frobenius version; and it seems likely
that the situation for other inductive types would be similar.

But I’m not sure, and I feel I may be overlooking or forgetting something
obvious.  What have others on the list thought about this?  Does anyone
have a reference discussing the Frobenius versions of inductive types other
than identity types, or at least giving the rules for them?

Best,
–Peter.

References:

- Gambino, Garner, 2008, “The Identity Type Weak Factorisation System”,
https://arxiv.org/abs/0803.4349
- van den Berg, Garner, 2008, “Types are weak  ω-groupoids”,
https://arxiv.org/pdf/0812.0298.pdf
- Gambino, Sattler, 2015, “The Frobenius condition, right properness, and
uniform fibrations”, https://arxiv.org/pdf/1510.00669.pdf

-- 
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: 5167 bytes --]

^ permalink raw reply	[flat|nested] 9+ messages in thread

end of thread, other threads:[~2020-05-16  8:34 UTC | newest]

Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2018-07-12 15:15 [HoTT] What is known and/or written about “Frobenius eliminators”? Peter LeFanu Lumsdaine
2018-07-12 17:06 ` Valery Isaev
2018-07-13 10:38   ` Peter LeFanu Lumsdaine
2018-07-13 11:05     ` Valery Isaev
2020-03-23  9:54       ` Ambrus Kaposi
2020-05-16  8:34         ` Rafaël Bocquet
2018-07-12 17:42 ` [HoTT] " Matt Oliveri
2018-07-12 18:06 ` [HoTT] " Thorsten Altenkirch
2018-07-12 18:23   ` Valery Isaev

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).