[HoTT] 1D W Type?

[Corlin Fardal <fardalcorlin@gmail.com>]

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

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.

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