- Overall comments.

This is a good paper: short but focused, and mathematically very careful.  I have no hesitation in recommending acceptance, with minor revisions (one correction and several suggested clarifications, as described below).

The results are original, and are an important building block in the author's current programme for a more general and rigorous model theory of type theory.

Unfortunately, this context is nowhere explained in the paper.  For a reader who has not been following the author's other recent writings and talks, it might be rather difficult to appreciate the motivation or importance of the present constructions (especially in relation to existing literature on categorical models of type theory).  It would be helpful if the author would consider adding a brief sketch of this motivation, or at least a pointer to somewhere it can be found.

* It is a very difficult task to analyze the earlier works on the categorical models of type theory. I believe that the importance of the present construction will be seen in relation not so much to the past works as to the works that are being released now and that use this construction as a starting point. I added a paragraph to the introduction connecting the main construction of the paper to the univalent model of the Martin-Lof inference rules.

Other than this, I found the presentation excellent: dry, but very clear.

- Significant mathematical queries

In Example 3.8, doesn't the category need to be a small category (in classical terminology), or a set-category (in the Ahrens-Kapulkin-Shulman terminology)?  The construction of the presheaves U and U-tilde seems to require that the objects of C comprise a set (taken as a restriction of size or of h-level, depending on whether one works in the classical or the univalent setting).

+ (Rem. 6.3, 6.4 )

The remark following Lemma 3.4 is rather unclear.  Am I right in reading it as saying that CC(C,p) depends only on the category C and morphism p, and NOT on the choice of universe structure or terminal object?  This is not clear as written, since up to here, p has been used in Def 2.3 and onward to mean a morphism together with universe structure, and (C,p) has been taken in the notation CC(C,p) to implicitly include a choice of pt.  Perhaps make the "..and does not depend on.." part more explicit, and also point out how this follows from Lemma 3.4 (i.e. by applying the lemma to the identity functor with the identity isomorphisms).

+ (now there is Example 4.9, is it sufficiently clear? Anything more precise can only be said in the language of the univalent foundations. There, there are two theorems:

1. The function (C,p,p_{X,F},Q(F),pt) -> CC(C,p,….) factors through the Rezk completion function on the input data.

2. The forgetting function (C,p,p_{X,F},Q(F),pt) -> (C,p) is of h-level 1 (an inclusion) over pairs (C,p) where C is a category (as opposed to a general precategory).

)

The style of the paper in places strongly suggests that it may have been (in whole or in part) formalised, or at least written with formalisation in mind.  Is that so?  If so, it would be of interest to mention it at least briefly.

+ (There is now a comment about the formalization-ready style in the introduction. We do not know yet when or 
by whom the paper will be formalized so I think this is better not to mention)


- Small mathematical points, typos, etc.

p.1, Introduction, para 1, "The type of the C-systems.."  Second "the" is erroneous.

+

p.1, Introduction, para 1, "slightly different from the Cartmell's.."  Again, erroneous "the".

+

p.1, Introduction, para 2, "type theories of the Martin-Lof genus." Would be more natural without the "the"; also, missing umlaut on Martin-Lof.

+

p.2, para 1, "..the only known construction of a C-system from a category level data..".  Erroneous "a" before "category level data".

+

p.2, same place as previous.  This remark could reasonably be strengthened: this is not just the only known such construction of a C-system, but more strongly, of any equivalent structure; i.e. no such construction has previously been given for contextual categories (to this reviewer's knowledge), which have a rather more extensive prior literature than C-systems.

+

p.2, para 5, "..we write the composition of morphisms of categories in the diagrammatic order.."  Given this choice, would the author consider using a symbol other than "\circ" for it?  "\circ" is strongly associated (in this reviewer's impression) with the categorical order (as is "\cdot"); diagrammatic-order composition is much more often denoted by a semi-colon, or just juxtaposition.

- There is already a paper in print where I made this choice and argued for it. 

p.2, last para of Introduction: "I am grateful to The Centre for Quantum Mathematics and Computation.."  "The" should not be capitalised.

+

p.3, Example 2.2, line 3, "the unit object of G": perhaps "unit element", since G is not a category?

+

p.3, last para, "One starts with Ob_0 = Hom(pt,pt).."  Is there an particular reason for using Hom(pt,pt) instead of some other singleton here?  It seems unnecessary and slightly unnatural.  It would fit better with subsequent notation to take Ob_0 = { () }, the singleton of the empty list.

+ (now using “unit” as the name of the set and “tt” as the name of its only element as is the done in Coq)

p.4, Construction 2.5, following definition of Hom_CC(C,p)): perhaps mention that "int" will always be explicitly written for the mapping from Hom_CC to Hom_C, even though it is a no-op.  As stands, this is a little disconcerting the first time one encounters it.

+/- this is not an issue in the new more detailed version of the construction since there int on morphisms is
not an identity function. 

p.4, construction 2.5, last para, last inline equation: f \circ Q(F_{m+1}) should be Q(int(f) \circ F_{m+1}).

+ (thanks, corrected. Now eq. (7) p. 6 )

p.5, above diagram (3): "are pull-back" should be "are pull-backs".

+ (middle of p. 12 now)

p.5, last line, "The fact that this construction gives a functor i.e. satisfies.."  Erroneous inter-sentence spacing after "i.e.": should be "i.e.\ satisfies" in TeX source (and elsewhere, whenever "i.e." is followed by a space).

+ all of the many “i.e.” are now in the form “…, i.e., “ which fixes the spacing issue.


p.6, Lemma 3.4, "..the corresponding solution of Construction 3.3.."  Perhaps "instance" instead of "solution"?  It seems odd speaking of the Construction as having solutions, since it itself is the solution of the preceding Problem.

+ (now Lemma 4.8) The wording is changed to, I hope, a more clear one.

p.6, Lemma 3.4, "..phi and phi-tilde are isomorphisms.."  The condition that phi-tilde is an iso is redundant, since it is a pullback of phi.

+ (see Lemma 4.8)

p.6, Lemma 3.4, "Then if Phi is [..] then H is [..]."  One of these "then"s should be removed.

+

p.7, Construction 3.6: The universe constructed here has been considered before, for closely related purposes, notably in Theorem 4.1 of Martin Hofmann, "Syntax and semantics of dependent types", in "Semantics and logics of computation", ed. Dybjer, Pitts, 1997.  It would be good to give some reference to this.

+ I think you mean Section 4.1 not Theorem 4.1. The construction there is, however, different as he suggests to take for Ty(Gamma) the ``set’’ of presheaves over C/Gamma which will be “large” relative to C while the construction that I use gives Ty that is of the same size as C.  


p.7, para 3, "we identify morphisms [..] with F(Gamma)."  Perhaps clearer: "..with elements of F(Gamma)."

+ In the new versions all of these bijections are explicit

p.7, Lemma 3.7, "Let Gamma' \in Ob(CC).." should be "..\in Ob_{>0}(CC).."

+ corrected (now Lemma 5.3)

p.8, Example 3.8, para 2, "The functoriality is defined by compositing f." Should be either "..by composing with f" or "..by composition with f".

+ now given explicitly, p. 28

p.8, para before Definition 3.9: "..the change in the choice of pull-backs.."  Should be either "..a change.." or just "..change.." (no article).

+/- This statement is not in the new version. 

p.8, same para: "the change of the C-system by a constructively isomorphic one"  More natural as "the replacement of the C-system by a constructively isomorphic one."

+/- This statement is not in the new version. 

p.8, same para: surely it is really the "will lead to", not the isomorphism, which is constructive?

+/- This statement is not in the new version. 

p.8, Conjecture: perhaps number this, since everything else in the paper is so consistently numbered?

+ Fixed. 

p.9, reference [1]: second author's name is given as Krzysztof Kapulkin (not Chris) on the cited paper; perhaps follow that here?  (I do not know which Kapulkin prefers to use in general, however, so if the author has inside knowledge, of course disregard this comment.)

+ Fixed.

p.9, reference [5]: date range should use an en-dash not a hyphen ("2009--2012" in LaTeX source).

+ Fixed.