Type theory is actually a stronger axiomatic system than ZFC, and is equiconsistent with ZFC+ a stronger condition.

See this mathoverflow response here https://mathoverflow.net/a/437200/477593