Three-HITs

Three-HITs copied to clipboard

Types of paths in computation rule for paths

2

Coq is asking me why the left and the right side of the equation at the bottom of page 3 (the one that says 'apD Hrec (p_i a) = q_i...

andrejbauer

Where do we rely on the boudned nesting of constructors

4

Somewhere in the proof we presumably rely on the fact that there is a bound on how deeply the point constructors are nested in the path constructors. Where? (I do...

andrejbauer

Explaining the construction

14

In Section 3, it is not explained anywhere what the purpose of all the data for the construction is. For instance, what are `Q` and `R` and `j_Q` about? These...

andrejbauer

Getting rid of parameters

3

There is currently quite a lot of confusion in the paper. I am going to list the problems I see, but it's probably a bad idea to try to fix...

andrejbauer

I am confused

4

Correct me if I am wrong, but aren't we doing the case of HIT which can be factored out into an ordinary inductive type followed by a coequalizer? If not,...

andrejbauer

Why separate the recursive and non-recursive constructors?

1

What is the purpose of separating the recursive and nonrecursive constructors? This should not be necessary. Also, where is the notion of "nonrecursive" and "recursive" constructor defined?

andrejbauer