[HoTT] Re: 1D Mu Type

["András Kovács" <puttamalac@gmail.com>]

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

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 
<https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/Functor1HIT.agda>
 with this change and a bunch of other stylistic changes.

You might be interested in this paper 
<https://pdfs.semanticscholar.org/6c81/a5233174e227d2d34270e1bdc15aae458df7.pdf>
 and demo implementation 
<https://bitbucket.org/akaposi/elims/src/dfa285fa6ba105b9cb1b9d9cc0601b239561f2d4/haskell/elims-demo/> 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 
<https://github.com/AndrasKovacs/misc-stuff/blob/master/agda/Simple1HIT.agda>. 
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.
>>
>

-- 
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: 9458 bytes --]