Hi,

Corlin Fardal: I've looked at the Agda version, it seems fine to me, but I think it's a bit more complicated than necessary. In particular, there's no need to parametrize TCode with an F-algebra. I wrote a version of my own here with this change and a bunch of other stylistic changes.

You might be interested in this paper and demo implementation about syntax and induction for higher inductive-inductive types (HIIT), which covers the current cases. Now, the formalization of this HIIT syntax is pretty heavyweight, but the general approach can be scaled back to 1-HITs, and then it becomes quite nice and straightforward to formalize in plain Agda, which I have here. It's moderately more general than your 1-HITs (e.g. it includes W-types), and it can be formalized without function extensionality.

András Kovács

On Tuesday, August 21, 2018 at 1:12:01 PM UTC+2, Niels van der Weide wrote:

Looks interesting!

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.
I think this is might be a special case of the work by Kaposi/Kovacs on HIITs. See
http://drops.dagstuhl.de/opus/volltexte/2018/9190/pdf/LIPIcs-FSCD-2018-20.pdf
They gave a syntax allowing both higher paths and function types.

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.
In addition, see the paper 'Quotient Inductive Inductive Types' by Altenkrich, Capriotti, Dijkstra, Kraus and Forsberg. Not all HITs are constructible as quotients, because that would require AC. This is because function types are added to the syntax. Section 9.1 in Lumsdaine&Shulman's Semantics of Higher Inductive Types also gives a counter example. Again note that they use a function type in the constructor sup.

On Saturday, August 18, 2018 at 11:30:53 PM UTC+2, Corlin Fardal wrote:
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.