I've managed to create a 1D Mu Type, essentially just a basis for creating 
any recursive higher inductive type with point and path constructors one 
could define. The construction is mainly based upon the paper "Higher 
Inductive Types in Programming," 
at http://www.cs.ru.nl/~herman/PUBS/HIT-programming.pdf. The construction 
reduces the path constructors to just one, by introducing a case term, and 
extends the polynomial functors to include function types, and introduces 
an application term and lambda term for the function types. To be able to 
deal with the new terms, the construction defines a type coercion function 
to make the path computation rule type check, but the way that it is 
defined makes it equal to the identity function, under case analysis that 
would compute down for any specific type. More details, of course, are in 
the Coq and Agda files attached to this post.

With this type we have a starting point for many next steps, including 
exploring the semantics of this new type, including showing that it gives 
rise to a cell monad, and showing homotopy initiality. Another next step 
would be seeing if we can define this type through some clever use of 
quotient types, perhaps in a similar way to the construction of 
propositional truncation.

I didn't write a paper about this, largely because it is just a fairly 
straight forward extension of an existing paper, and also because I'm not a 
terribly good writer, but I hope that this post suffices in sharing what 
little I've managed to accomplish. I also hope that this post doesn't seem 
too out of the ordinary for what's posted here, as this is the first thing 
I've ever posted, and I'm very new to this group in general, though I have 
read a good few things on here already, and from what I can tell, this 
doesn't seem too strange.

I checked various cases of HITs with my Mu type, and while the various 
constructors and induction rules seem to align with my intuition for what 
they should be, I don't actually know of anywhere where the induction rules 
for various kinds of inductive types exist, so I'd like to know if the 
definitions are correct, or if I messed anything up. In general, I'd be 
interested in anyone's thoughts about this.

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