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:43:41 +1000
Authentication-results: mail3-smtp-sop.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-f193.google.com
Ironport-phdr: 9a23:67CeQRQPRheC7kDWvHZsn4cLm9psv+yvbD5Q0YIujvd0So/mwa69YhKN2/xhgRfzUJnB7Loc0qyK6vymADRfqs7Y+Fk5M7VyFDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjeu8UMnIduNqQ8xhTVrndVZu9b2X5mKVWPkhnz4cu94IRt+DlKtfI78M5AX6T6f6AmQrFdET8rLWM76tD1uBfaVQeA6WcSXWsQkhpTHgjK9wr6UYvrsiv7reVyxi+XNtDrQL8uWDSi66BrSAL0iCoCKjU0/n3bhtB2galGux+quQBxzJDIb4GULPp+f73SfdUGRWpaQ81dUzVNDp6gY4cTCuYMO/tToYvgqFsUtRaxCgesC+HvxDFGhXH4wLM03Pg6HA7cwAAtBcgDvGjIoNj3MqoZTOC7zLPPzTXGd/5YxCv955bWch8/p/GHQK9+ccrLxkghCgjIiU6QqZD7MDOLyOsNtXOW7/F8Ve2xkG4nqxt+oza1yscrkInJiZsYx1bZ/it62IY4PcO0RFJ/bNK+E5ZdtzuWO5VoTs88WW1kpSI3x7MAtJWmZiYF0o4nyATaa/Gfc4iH/BbjVOGJLDd9nn1leba/iw+r8Uij1+HwT8e03EtOoydLiNXMuXcN1xvc6siDVPRx5Fuu2TGK1wzL6+FEJ147lbbDJpI/3rI9koAfvEfDEyPshkn6krGael859uWs5enrerDmqYWdN49whAH+KKMumsmnDOQjLggBQXab9vq61LD45k35XKtFjuY2kqbDvpHWP8MbprS2AwNNyIYs9w6/Dyu60NQfhXQIMFVFeAueg4f1P1HOPev3AOykg1WslTdr3+rJMqfgApXLNHjDka3ucaxz605Gm0IPyoV97olTDPkuOvXoQQelttXDCRk2KQuv2LfPB9B014dYUmWKVPy3KqTX5GSU6/wiJaG3ZIYK8GLmN/U76vjGlmM0gl8UYu+ux5RBOyPwJehvP0jMOSmkudwGC2pf+1NmFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKaHdK2nLGa3C6kWJpMaTIeUw3eITLTb4yBHsw0RmeSL8tmyGJWULGgT8o41kjrularkPxoKe3b/iBevpXmhoAsu7/j0Coq/DkxNPyzlnmXRjgvzHgUSiQ21b85plZymA+O

An additional advantage of Type Theory is that it maintains the abstraction barrier, whereas, in Set Theory, you can look inside to see how your mathematical objects are encoded as sets.

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
        
        Re: [Coq-Club] [Agda] [lean-user] Re: Why dependent type theory?, Stefan Monnier, 03/15/2020