There are other proof assistants based on type theory. We have Lego which is based on a different extension of the calculus of constructions; we have the family of proof assistants based on Martin-Löf type theory and developed essentially at Cornell University; we have the NuPRL proof assistant with is based on an extensional version of Martin-Löf type theory and developed at Cornell.

---