I've been playing around with a potential general 1D W Type, but I've run across one problem. To give some quick exposition first though, I thought about what it would look like to W-ize the 1D Mu Type posted here a few weeks ago, and realized relatively quickly that it would look more-or-less like the following: data W (F G : Cont) (f g : {X} -> (ContInter F X -> Set) -> Morph G Id) where c : (x : ContInter F (W F G f g)) -> W F G f g e : (x : ContInter G (W F G f g)) -> MorphInter (f c) x = MorphInter (g c) x with some predefined notion of Cont, Morph, and the related terms. Now, Cont should obviously be the standard container found in the standard W type, and Morph seems at first blush like it should be a container morphism, and that almost works. Almost every term the Mu type uses can be pretty straightforwardly defined as a container morphism, but for one: con, the representation of c itself. Now in some ways this seems somewhat obvious, the notion of container morphism is pretty general, and isn't designed including the constructor c, as the syntactic notion of terms are in the Mu type. However, it feels like it should be possible to modify the notion of morphism to suit the needs of representing c, though how exactly that would be done seems somewhat non-obvious to me. So, I guess my question is, can anyone come up with some natural extension of the morphism that accounts for c, or perhaps I'm coming at this from the wrong angle, and there's some other obvious route that I'm missing. -- 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.