<div dir="ltr"><div class="gmail_default" style="font-family:arial,sans-serif">I really enjoyed the following video with Thorsten Altenkirch which speaks informally about Type Theory and Set Theory:<br></div><div class="gmail_default" style="font-family:arial,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,sans-serif">  <a href="https://youtu.be/qT8NyyRgLDQ">https://youtu.be/qT8NyyRgLDQ</a></div><div class="gmail_default" style="font-family:arial,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,sans-serif">The follow-up video has some further commentary <a href="https://youtu.be/SknxggwRPzU">https://youtu.be/SknxggwRPzU</a>.</div><div class="gmail_default" style="font-family:arial,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,sans-serif">Since you're writing a thesis with a focus on Coq, I'm sure you understand the details. You might enjoy the informal distinctions between Type Theory and Constructive Mathematics vs Set Theory and Classical Logic.</div><div class="gmail_default" style="font-family:arial,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,sans-serif">I would summarise that Constructive Mathematics (using Type Theory) is better because it provides more confidence in your proofs.</div><div class="gmail_default" style="font-family:arial,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,sans-serif">Best,</div><div class="gmail_default" style="font-family:arial,sans-serif">Steve.</div></div>