nmvdw/three-hits

All higher inductive types can be obtained from three simple HITs.

three-hits's Issues

Getting rid of parameters

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 each one separately without thinking of the paper as a whole. Here's one.

In Section 3, the higher inductive types H_rec, H_Con^n etc. are parameterized by P. This does not make sense, first because P is an expression schema, and also because we only ever introduce non-parameterized types.

I also find the entire construction very hard to follow because of the notation. It would be better to fix P and n and all the other things that the type depends on, and then not mention them in the names of constructions.

Types of paths in computation rule for paths

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 a (Bi Hrec a)`) have the same type. Is this supposed to be obvious?

In the formalization we'll have to insert a transport becaue the computation rule for points is not judgmental (we can't express judgmental equality like that), but I'd first like to understand why the equation is supposed to make sense in the paper.

In concrete examples the types seem to match, although (somwhat amazingly), all point constructors in the HoTT library that I could find were non-recursive and so they're much more easily handled.

Abstract

Colimits in HoTT

There is an outstanding PR request for a colimits library in HoTT, see HoTT/Coq-HoTT#850. We probably shouldn't duplicate the effort needlessly.

Where do we rely on the boudned nesting of constructors

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 not mean the n in the definition of H_Con^n, I mean where do we need the fact that there is such an n?)

Lemma 13

Lemma lem:pathext is not proven correctly. I am not sure whether the current formulation is correct.

Definition of a constructor term over a given `c`

The definition of a constructor term (labeled def:constructor-term) seems fishy. They way it's written, I can come up with any term e whatsoever, and then claim that π₁(e, e) is a constructor term. What was actually meant here?

Also, the premise that c : A T → T is a function is not clear. What is A? What is T?

Explaining the construction

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 symbols are not connected to anything that came before, or I just don't see it.

I think it would help to see how the construction works in a particular simple example.

Colimit via sigma and coequalizers

Conjecture: Given are F : N -> Type and f : Π n : N, F n -> F(n+1). Define C = Σ n : N, F n. Note we have a map i : Π n : N, F n -> C sending x : F n to (n, x). Define g_1 : Σ n : N, F n -> F n to be Σ n : N, (i (n+1)) o f n and g_2 : Σ n : N, F n -> F n to be Σ n : N, i n . Then hocolim F f is isomorphic to the coequalizer of g_1 and g_2.

I am confused

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, what's a counter-example? Our signature is finitary, so it ought to be the case that we can just do it this way.

Which begs the question: what is the paper about then?

(I probably asked you this question already in Ljubljana. For forgetful people like me, we should provide a counter-example in the paper.)

Why separate the recursive and non-recursive constructors?

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?