Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Valery Isaev <valery.isaev@gmail.com>
To: Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>
Cc: "HomotopyTypeTheory@googlegroups.com"
	<homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
Date: Thu, 12 Jul 2018 20:06:45 +0300	[thread overview]
Message-ID: <CAA520fskvdGLzpq=u_3NhtHfLcvCTtpexBPygyNK85XGh71Qzg@mail.gmail.com> (raw)
In-Reply-To: <CAAkwb-mM5z4_ihJy0+VTgmkk17J7w2E62YDy5QSnn51vhvk1gg@mail.gmail.com>

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

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. I did not
write down proofs in full detail, but I sketched them for identity types,
sigma types, and coproducts and I think this also should be true for
pushouts. Now, when I say that we have identity types I mean a strong
version of Id:
Γ |– a : A
Γ, y:A, u:Id(a,y)  |– C(y,u) type
Γ |– d : C(a,a,r(a)) type
Γ |— b : A
Γ |— p : Id(a,b)
——————————————
Γ |— J(a, (y,u)C, d, b, p) : C(b,p)

We can prove all the usual constructions for identity types using this
version of J including transport and extensionality for sigma types. To
define the "Frobenius version" of this J, we construct a term t : (b,p) =
(a,r(a)) using extensionality for sigma. Then we transport c along t
from Δ(b,p) to Δ(a,r(a)), and substitute this in d. At this point, we have
a term d' of type C(a,r(a),t_*(c)). Then we use the fact that the type of
triples \Sigma (q : \Sigma (b : A) Id(a,b)) Id((b,p),q) is contractible
(this type is of the form \Sigma (x : A) Id(a,x) and we can prove that such
types are contractible using the strong version of J). Thus, we have a path
from ((a,r(a),t) to ((b,p),r((b,p))) and transporting d' along this path
gives us a term of type C(b,p,c).

Similar argument shows that the "Frobenius version" of sigma eliminator is
definable. We just prove that p = (\pi_1(p),\pi_2(p)) and then transport
terms back and forth along this path. The proof for coproducts is slightly
more difficult, but the idea is similar.

I constructed Frobenius versions of various eliminators in my recent
preprint https://arxiv.org/abs/1806.08038 (I call Frobenius eliminators
"local" and the usual ones "global"). I used there a non-standard version
of HoTT, but as I mentioned before I believe that it should be possible to
construct them in the ordinary HoTT (with sigma and Id types only).

I also want to mention that Frobenius eliminators are definable only when
our constructions are stable under substitution. If we do not assume that
the type former, the constructors, and the non-Frobenius eliminator of some
construction are stable under substitution, then we can interpret them in
any category in which the corresponding categorical constructions are not
necessarily stable under pullbacks, but this is not true for Frobenius
eliminators.

2018-07-12 18:15 GMT+03:00 Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>:

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


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

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

  reply	other threads:[~2018-07-12 17:07 UTC|newest]

Thread overview: 9+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-07-12 15:15 Peter LeFanu Lumsdaine
2018-07-12 17:06 ` Valery Isaev [this message]
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

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAA520fskvdGLzpq=u_3NhtHfLcvCTtpexBPygyNK85XGh71Qzg@mail.gmail.com' \
    --to=valery.isaev@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=p.l.lumsdaine@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).