coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Agda] Why dependent type theory?

From: Steven Shaw <steven AT steshaw.org>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>, agda-list <agda AT lists.chalmers.se>, coq+miscellaneous AT discoursemail.com, lean-user <lean-user AT googlegroups.com>
Subject: Re: [Coq-Club] [Agda] Why dependent type theory?
Date: Wed, 4 Mar 2020 08:32:24 +1000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=steven AT steshaw.org; spf=None smtp.mailfrom=steven AT steshaw.org; spf=None smtp.helo=postmaster AT mail-qk1-f195.google.com
Ironport-phdr: 9a23:EHqjGBxlKSBXMxrXCy+O+j09IxM/srCxBDY+r6Qd2+oVIJqq85mqBkHD//Il1AaPAdyHrasc1aGP7fyocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLx/IA+roQnNt8QajpZuJ6c+xxDUvnZGZuNayH9nKl6Ugxvy/Nq78oR58yRXtfIh9spAXrv/cq8lU7FWDykoPn4s6sHzuhbNUQWA5n0HUmULiRVIGBTK7Av7XpjqrCT3sPd21TSAMs33SbA0Ximi77tuRRT1hioLKyI1/WfKgcFrkqlVvAyuqAB+w47MYYGaKvx+fr/GfdgHQWZNR9tdWzBdDo+5aYYEEugPMvtCr4TlqFQOoxmxCwmiCu3s1zFGmGP50LYg3Og9CwzLxhAsE84MvXnSsd77NL0SUeewzKTQ0DvDc+1Z2Snj54jObxsvvPGMUqh+cMHMzkQvDB/FgUuOqYP7OTOYzf8Ns3SF4Op7VeKgkWAmpxt2oji1ycchk4/EjZ8bxFDD8CV22oc1JdugRU97Zt6kDYdQtzyAO4RtXMwvRXxjtiUiyrAep5K3YCwHxI4kyhPfcfCLbZaE7gz5WOqMJTp1hHRoc6+liRmo60iv0Oj8W9G00FlUqipFlcHBtnUX2BzS7siLU+J9/kS81TqW2QDf9+VJLEAumarULJ4hxbEwlp4NvkjZAiD2n0D2gLeXdkUi5Oeo9/zqbqv6qpKYLYN5iQHzPr4wlsChH+g0KBUCUmyb9Oik0b3s50z5QLFEjv0slanZtYjXJd8HpqGnHQ9azIAj5g2kDze6ztsYhnkHI0hLeR6diIjpIV7OLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g6EXQmWJSoCDN7jJ+QuK7/koJeaWY5QO6R7yLvEk47jlinpvynEHeqz85ocadn2+Vs9mKlrRNWHwj8kMF08RogclTOX1zlqYXmgAND6JQ6sg62RjW8qdBoDZS9Xo2eTZhXvpLthtfmlDT2u0PzLwbYzdAKUXdC+JIsZ+1DseWur5Et5z5VSVrAb/joFfAK/R8ywcu4jk0YEutfbPmAoy/CMyCN6SgTnUEjNE21gQTjpz55hR5ExwzlDZj/p9iv1cUMVQvrZHC1Znc5HbyON+Bpb5XQeTJto=

I really enjoyed the following video with Thorsten Altenkirch which speaks informally about Type Theory and Set Theory:

The follow-up video has some further commentary https://youtu.be/SknxggwRPzU.

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.

I would summarise that Constructive Mathematics (using Type Theory) is better because it provides more confidence in your proofs.

Best,

Steve.

Re: [Coq-Club] Why dependent type theory?, (continued)
- Re: [Coq-Club] Why dependent type theory?, Christian Doczkal, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Ken Kubota, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, jonikelee AT gmail.com, 03/03/2020
- Re: [Coq-Club] Why dependent type theory?, Daniel Schepler, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, mechvel, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Steven Shaw, 03/03/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/03/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Sylvain Boulmé, 03/04/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Kevin Buzzard, 03/05/2020
    - Re: [Coq-Club] [lean-user] Re: [Agda] Why dependent type theory?, Bas Spitters, 03/08/2020
      - Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/12/2020
        
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Mario Carneiro, 03/13/2020
        
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Kevin Buzzard, 03/13/2020
        
        Message not available
        
        Message not available
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Bas Spitters, 03/17/2020
        
        Message not available
        
        Message not available
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Thorsten Altenkirch, 03/18/2020