Is Martin-Lf type theory basically the predicative Calculus of inductive Constructions without impredicative $\mathtt{Prop}$?If they're closely related but with more differences than just $\mathtt{Prop}$, what are those differences?
Is MLTT effectively pCiC without Prop?
type theory;calculus of constructions
The short answer is yes, MLTT can reasonably be equated with CIC without impredicative Prop.The main technical issue is that there are dozens of variants when one talks about Martin-Lf Type Theory and, perhaps more surprisingly, when one talks about CIC. For example, taking the version of CIC defined in Benjamin Werner's thesis, it doesn't even make sense to remove Prop, as one doesn't have either Set or universes of Type.The main variations one can consider in either of these theories are:Universes: how many, and how are they defined (Palmgren, On Universes in Type Theory, discusses many inequivalent variations), and whether or not universe polymorphism is admitted.Which inductive types/families: Agda admits Inductive-Recursive types, but there are many more mundane variations depending on how large the types in the constructors and eliminators are allowed, handling parameters vs indices, etc.Injectivity of type constructors. This leads to a system inconsistent with EM in Agda. Of course Epigram has a more extreme Observational Type Theory, but this can be considered something different altogether.Axiom K: this comes for free with certain versions of dependent pattern matching.Intentional vs Extensional: this is a huge difference, where essentially a new conversion rule is added in the extensional systems$$ \frac{\Gamma\vdash t:\mathrm{Id}_{\mathrm{Type}}\ A\ B }{\Gamma\vdash A\ =\ B} $$Which makes type-checking undecidable (but much more powerful!). Martin-Lf himself seems to have considered both types of systems.The presence of coinductive types and associated elimination principles.All of the above variations (except OTT) have been considered in the literature and associated with the name Martin-Lf Type Theory or Calculus of Inductive Constructions, mostly because of their association with the Agda and Coq systems, respectively.So the long answer is that there is no consensus about what the exact definition of either of these systems is.