Return to Answer

I would not align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

I would not align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

I do not think I would align typed conversion with CiC versus MLTT. From my perspective, the move from untyped to typed conversion is simply an example of technology improving over time. While it wouldn't be trivial, producing a version of CiC with typed conversion seems like a fairly routine effort.

IMO, the serious difference in design lies in the treatment of Prop. Coq (and Lean) have an impredicative sort of propositions, and this really fundamentally changes the logical strength of the theory.

You can formalise the normalisation of System F in Coq/Lean, and you just can't in predicative systems like Agda. Conversely, the metatheory of predicative systems like Agda is much simpler to establish than that of CiC-style systems.

One thing which does seem like a cultural difference to me is that Agda/Idris favour top-level clausal definitions, whereas Coq has a more traditional expression-oriented design. (E.g., Agda doesn't even have a case expression AFAIK.)

There might be a slight technical basis to this choice (polarised presentations of type theory tend to lead one towards clausal definitions), but it mostly seems to be based on whether the proof assistant was implemented in Haskell (lots of clausal definitions) or ML (lots of expressions).