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: on behalf of Peter LeFanu > Lumsdaine > Date: Thursday, 12 July 2018 at 16:15 > To: "homotopytypetheory@googlegroups.com" googlegroups.com> > 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. > 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 > message in error, please contact the sender and delete the email and > 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. > 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.