coquand

Thanks for this very simple example! When writing the rules for propositional truncation, we discovered that the implementation of recursive HIT is not correct. The problem here should be in...

Thanks again for this other simple example. We have been mainly working on the presentation of the type system (for HIT spheres and propositional truncation) and did not try yet...

I did not have time to react before, but this might be an issue since we then loose a natural way to have inductive-recursive definitions. > On 29 Jul 2016,...

What do you mean by “multiple levels of nested mutual blocks”? The example I had in mind was something like mutual data V = n | pi (x:V) (f:El x...

Maybe I misunderstood: is this connected to the optimisation suggested by Guillaume or it is a different thing? > On 29 Jul 2016, at 16:00, Anders Mörtberg [email protected] wrote: >...

Thanks for the example. I am not sure it should type-check however. The type-checking of a recursive definition x : A = t should be x : A |- t...

For this example they should not be needed since the type S1 is a constant type and so one can use the identity function for “forward”. But it is not...

Semantically this is not justified since e.g. if we define g : S1 -> A from a : A and l : Path A a a by g base =...

> On 9 Jun 2017, at 17:57, Jonathan Sterling wrote: > @coquand Thank you for the very helpful comments. I have a question about this failure of confluence... > >...