I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers.
But I haven’t heard of a type-theory based automated theorem prover (nor of a sequent-calculus based proof-checker). Does a type-theory based ATP exist? (And a sequent-calculus based proof-checker?)
If not, why is it that type theory is more fit for proof-checking, and sequent-calculus more fit for proof-finding?