Set-like mathematics in type theory — LessWrong