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)

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

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.

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

[-- Attachment #2: Type: text/html, Size: 5167 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
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-12 17:42  [HoTT] " Matt Oliveri
2018-07-12 18:06  [HoTT] " Thorsten Altenkirch
From: Valery Isaev @ 2018-07-12 17:06 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine; +Cc: HomotopyTypeTheory@googlegroups.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
>
> 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.

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

[-- Attachment #2: Type: text/html, Size: 9403 bytes --]

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

* [HoTT] Re: What is known and/or written about “Frobenius eliminators”?
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-12 17:42  Matt Oliveri
2018-07-12 18:06  [HoTT] " Thorsten Altenkirch
2 siblings, 0 replies; 9+ messages in thread
From: Matt Oliveri @ 2018-07-12 17:42 UTC (permalink / raw)
To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 5913 bytes --]

This looks similar to the "left rule" version of inductive elimination,
where you eliminate a variable (not an arbitrary term), and the context
extension depending on it gets updated. Except the "Frobenious version"
allows an arbitrary term, so you say in what way part of the context
depends on it. (Your "c : Δ(a,b,p)".) Coq's "destruct" tactic sort of
implements this; it picks Δ and c for you by searching subexpressions in
the context. In general, "dependent pattern matching" seems to use the left
rules, and variants, rather than the "simple versions", where the context
never changes. Have you tried looking at the literature on dependent
pattern matching? I know this isn't a real answer. I don't know any papers
that I know have Frobenious versions. Also, it looks like your Δ is not
literally a context extension, but the corresponding dependent record type.

On Thursday, July 12, 2018 at 11:15:38 AM UTC-4, Peter LeFanu Lumsdaine
wrote:
>
> 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
>
> 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.
>
> (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
> 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.

[-- Attachment #1.2: Type: text/html, Size: 7603 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
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-12 17:42  [HoTT] " Matt Oliveri
@ 2018-07-12 18:06  Thorsten Altenkirch
2018-07-12 18:23    Valery Isaev
From: Thorsten Altenkirch @ 2018-07-12 18:06 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine, homotopytypetheory

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

Isn't this what is usually called recursion with parameters. E.g. in the simple typed case for natural numbers: the usual recursor can be written using only 1st order functions:

z : X
s : Nat -> X -> X
-----------------------
R_X(z,s) : N -> X

R(z,s) 0 == z
R(z,s) (suc m) == s m (R(z,s) m)

while recursion with a parameter is:

z : Y -> X
s : Nat -> Y -> X -> X
----------------------------
R'_X,Y(z,s) : Nat -> Y -> X

R'(z,s) 0 y == z y
R'(z,s) (suc m) y == s m y (R'(z,s) m y)

Using functions we can reduce R' to R

R'_X,Y(z,s) = R_(Y -> X)(z,\n f y.s n y (f y))

but without functions R' is stronger and it is what you need to have recursion in every slice.  A simple example is addition over the 1st argument, which with functions we can write as

R_Nat->Nat (\n . n) (\ n fn m . suc (fn m))

but you can use R' without function types

R'_Nat,Nat (\ n . n) (\ n m x . suc m)

Hence in the absence of Pi-types you need to use the "localized" version of the recursor. I think in the special case of + this gives you distributivity over x even without cartesian closure.
If we don't assume products we need to replace Y by a context.

I think I have seen the case for Id in Thomas Streicher's habilitation but I am not sure.

Thorsten

Date: Thursday, 12 July 2018 at 16:15
Subject: [HoTT] What is known and/or written about “Frobenius eliminators”?

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<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

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

[-- Attachment #2: Type: text/html, Size: 9550 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
2018-07-12 18:06  [HoTT] " Thorsten Altenkirch
@ 2018-07-12 18:23    Valery Isaev
0 siblings, 0 replies; 9+ messages in thread
From: Valery Isaev @ 2018-07-12 18:23 UTC (permalink / raw)
To: Thorsten Altenkirch; +Cc: homotopytypetheory

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

Such version corresponds simply to the fact that the eliminator is defined
in every context (Γ in Peter's original post). Without this context
eliminators are undeniably too weak. The point of Frobenius eliminators is
that Y in your notation can depend on the eliminated parameter. I don't
think that it is possible to define Frobenius for recursive datatypes.

Regards,
Valery Isaev

2018-07-12 21:06 GMT+03:00 Thorsten Altenkirch <
Thorsten.Altenkirch@nottingham.ac.uk>:

> Isn't this what is usually called recursion with parameters. E.g. in the
> simple typed case for natural numbers: the usual recursor can be written
> using only 1st order functions:
>
> z : X
> s : Nat -> X -> X
> -----------------------
> R_X(z,s) : N -> X
>
> R(z,s) 0 == z
> R(z,s) (suc m) == s m (R(z,s) m)
>
> while recursion with a parameter is:
>
> z : Y -> X
> s : Nat -> Y -> X -> X
> ----------------------------
> R'_X,Y(z,s) : Nat -> Y -> X
>
> R'(z,s) 0 y == z y
> R'(z,s) (suc m) y == s m y (R'(z,s) m y)
>
> Using functions we can reduce R' to R
>
> R'_X,Y(z,s) = R_(Y -> X)(z,\n f y.s n y (f y))
>
> but without functions R' is stronger and it is what you need to have
> recursion in every slice.  A simple example is addition over the 1st
> argument, which with functions we can write as
>
> R_Nat->Nat (\n . n) (\ n fn m . suc (fn m))
>
> but you can use R' without function types
>
> R'_Nat,Nat (\ n . n) (\ n m x . suc m)
>
> Hence in the absence of Pi-types you need to use the "localized" version
> of the recursor. I think in the special case of + this gives you
> distributivity over x even without cartesian closure.
> If we don't assume products we need to replace Y by a context.
>
> I think I have seen the case for Id in Thomas Streicher's habilitation but
> I am not sure.
>
> Thorsten
>
>
> From: <homotopytypetheory@googlegroups.com> on behalf of Peter LeFanu
> Lumsdaine <p.l.lumsdaine@gmail.com>
> Date: Thursday, 12 July 2018 at 16:15
> Subject: [HoTT] What is known and/or written about “Frobenius
> eliminators”?
>
> 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
>
> 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.
>
> (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
> 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
> For more options, visit https://groups.google.com/d/optout.
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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
> 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.

[-- Attachment #2: Type: text/html, Size: 11066 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
2018-07-12 17:06  Valery Isaev
@ 2018-07-13 10:38    Peter LeFanu Lumsdaine
2018-07-13 11:05      Valery Isaev
From: Peter LeFanu Lumsdaine @ 2018-07-13 10:38 UTC (permalink / raw)

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

On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <valery.isaev@gmail.com> wrote:

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

Thankyou — very nice observation, and (at least to me) quite surprising!

> I mean a strong version of Id:
>

Side note: this is I think more widely known as the Paulin-Mohring or
one-sided eliminator for Id-types; the HoTT book calls it based
path-induction.

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

Ah, yes — there was a mistake in the argument I had in mind.  In that case,
do we really know for sure that the Frobenius versions are really strictly
stronger?

–p.

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

[-- Attachment #2: Type: text/html, Size: 2699 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
2018-07-13 10:38    Peter LeFanu Lumsdaine
@ 2018-07-13 11:05      Valery Isaev
2020-03-23  9:54        Ambrus Kaposi
From: Valery Isaev @ 2018-07-13 11:05 UTC (permalink / raw)
To: Peter LeFanu Lumsdaine; +Cc: HomotopyTypeTheory@googlegroups.com

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

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

> On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <valery.isaev@gmail.com>
> wrote:
>
>> 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.
>>
>
> Thankyou — very nice observation, and (at least to me) quite surprising!
>

I was surprised too. The case of coproducts is especially unexpected.

>
>
>> I mean a strong version of Id:
>>
>
> Side note: this is I think more widely known as the Paulin-Mohring or
> one-sided eliminator for Id-types; the HoTT book calls it based
> path-induction.
>
> 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.
>>
>
> Ah, yes — there was a mistake in the argument I had in mind.  In that
> case, do we really know for sure that the Frobenius versions are really
> strictly stronger?
>
> I don't know how to prove this, but it seems that we can't even define
transport without Frobenius J. Also, if we do have transport and we know
that types of the form \Sigma (x : A) Id(a,x) are contractible, then the
"one-sided J" is definable, so if we want to prove that the Frobenius
version does not follows from the non-Frobenius, we need to find a model
where either transport is not definable or \Sigma (x : A) Id(a,x) is not
contractible.

> –p.
>
>
>

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

[-- Attachment #2: Type: text/html, Size: 4303 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
2018-07-13 11:05      Valery Isaev
@ 2020-03-23  9:54        Ambrus Kaposi
2020-05-16  8:34          Rafaël Bocquet
From: Ambrus Kaposi @ 2020-03-23  9:54 UTC (permalink / raw)
To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 2885 bytes --]

Hi,

Sorry for resurrecting an old thread, I just wanted to document that
Frobenius J can be derived from Paulin-Mohring J without Pi, Sigma or
universes:
https://github.com/akaposi/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda
This was observed by Rafael Bocquet and András Kovács in October 2019, but

We mention this briefly in our paper on HIIT signatures where
Paulin-Mohring J can be used on previous equality constructors but we don't
have Pi, Sigma or (usual) universes: https://lmcs.episciences.org/6100

Cheers,
Ambrus

2018. július 13., péntek 13:05:47 UTC+2 időpontban Valery Isaev a
következőt írta:
>
>
> 2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine <p...@gmail.com
> <javascript:>>:
>
>> On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev <va...@gmail.com
>> <javascript:>> wrote:
>>
>>> 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.
>>>
>>
>> Thankyou — very nice observation, and (at least to me) quite surprising!
>>
>
> I was surprised too. The case of coproducts is especially unexpected.
>
>
>>
>>
>>> I mean a strong version of Id:
>>>
>>
>> Side note: this is I think more widely known as the Paulin-Mohring or
>> one-sided eliminator for Id-types; the HoTT book calls it based
>> path-induction.
>>
>> 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.
>>>
>>
>> Ah, yes — there was a mistake in the argument I had in mind.  In that
>> case, do we really know for sure that the Frobenius versions are really
>> strictly stronger?
>>
>> I don't know how to prove this, but it seems that we can't even define
> transport without Frobenius J. Also, if we do have transport and we know
> that types of the form \Sigma (x : A) Id(a,x) are contractible, then the
> "one-sided J" is definable, so if we want to prove that the Frobenius
> version does not follows from the non-Frobenius, we need to find a model
> where either transport is not definable or \Sigma (x : A) Id(a,x) is not
> contractible.
>
>
>> –p.
>>
>>
>>
>

[-- Attachment #1.2: Type: text/html, Size: 5026 bytes --]

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

* Re: [HoTT] What is known and/or written about “Frobenius eliminators”?
2020-03-23  9:54        Ambrus Kaposi
@ 2020-05-16  8:34          Rafaël Bocquet
0 siblings, 0 replies; 9+ messages in thread
From: Rafaël Bocquet @ 2020-05-16  8:34 UTC (permalink / raw)
To: HomotopyTypeTheory

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

Hi,

Here's a simple countermodel that shows that the Martin-Löf eliminator
(two-sided eliminator) for identity types is not strong enough to derive
transport in the absence of Pi-types.

Consider the initial model of a type theory with Id, refl, a closed type
A, a type family B over A, and closed terms x,y : A, b : B x and p :
Id_A x y.

It can be shown that the only terms of that model are the variables, the
weakenings of the generators and their iterated refls.

Because there is no closed term of type B y, transport does not hold in
this model.

However, unless I missed some cases, it is still possible to define the
Martin-Löf eliminator by case distinction on the elimination target.

Best,
Rafaël

On 3/23/20 10:54 AM, Ambrus Kaposi wrote:
> Hi,
>
> Sorry for resurrecting an old thread, I just wanted to document that
> Frobenius J can be derived from Paulin-Mohring J without Pi, Sigma or
> universes:
> https://github.com/akaposi/hiit-signatures/blob/master/formalization/FrobeniusJDeriv.agda
> This was observed by Rafael Bocquet and András Kovács in October 2019,
>
> We mention this briefly in our paper on HIIT signatures where
> Paulin-Mohring J can be used on previous equality constructors but we
> don't have Pi, Sigma or (usual) universes:
> https://lmcs.episciences.org/6100
>
> Cheers,
> Ambrus
>
> 2018. július 13., péntek 13:05:47 UTC+2 időpontban Valery Isaev a
> következőt írta:
>
>
>     2018-07-13 13:38 GMT+03:00 Peter LeFanu Lumsdaine
>     <p.l.l...@gmail.com <javascript:>>:
>
>         On Thu, Jul 12, 2018 at 7:07 PM Valery Isaev
>         <valer...@gmail.com <javascript:>> wrote:
>
>             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.
>
>
>         Thankyou — very nice observation, and (at least to me) quite
>         surprising!
>
>
>     I was surprised too. The case of coproducts is especially unexpected.
>
>             I mean a strong version of Id:
>
>
>         Side note: this is I think more widely known as the
>         Paulin-Mohring or one-sided eliminator for Id-types; the HoTT
>         book calls it based path-induction.
>
>                 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.
>
>
>         Ah, yes — there was a mistake in the argument I had in mind.
>         In that case, do we really know for sure that the Frobenius
>         versions are really strictly stronger?
>
>     I don't know how to prove this, but it seems that we can't even
>     define transport without Frobenius J. Also, if we do have
>     transport and we know that types of the form \Sigma (x : A)
>     Id(a,x) are contractible, then the "one-sided J" is definable, so
>     if we want to prove that the Frobenius version does not follows
>     from the non-Frobenius, we need to find a model where either
>     transport is not definable or \Sigma (x : A) Id(a,x) is not
>     contractible.
>
>         –p.
>
>
>
> --
> 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
> To view this discussion on the web visit

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/17a9e7e7-e03b-cf03-58de-5f1f77d74469%40ens.fr.

[-- Attachment #2: Type: text/html, Size: 12088 bytes --]

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

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

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