There are several other systems based either on the calculus of constructions (Lego, Matita, Lean) or on intuitionistic type theory (Epigram, Idris); see (Pollack 1994; Asperti et al. 2011; de Moura et al. 2015; McBride and McKinna 2004; Brady 2011).