coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] HoTT ideas already present in CIC?

From: José Manuel Rodriguez Caballero <josephcmac AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] HoTT ideas already present in CIC?
Date: Sun, 27 May 2018 17:06:45 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=josephcmac AT gmail.com; spf=Pass smtp.mailfrom=josephcmac AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f45.google.com
Ironport-phdr: 9a23:gx0VthcFs61slcmZA4SAIsM0lGMj4u6mDksu8pMizoh2WeGdxcu+bB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM28m/XhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b4YXC+QBOv1YqJPlqFUJtxS+AxSsC/3ryjBQmnH22rA10/4gEQHJwQwvAdMPv2zKodrvL6gdS+S1zK3WwjXZaPNdxDDw6IrPchA6v/6MRbJwftbUyUY1CwzIlVqQqYn/MDOU0uQBqXSU7+1lVe+2jWMstgJ/oiC3y8syloXEgpgZx1PE+Clj3oo5ONK1RFR0bNOkFpZbqjuUOJFsQsw4RmFloCY6xaMCuZ68ZCUKzY4oxx/ba/CecoiI/g7vWP+fITp3hH9pYr2/hxG18Uivzu3zSNO430pNripAitXMt3YN2ALP6sWfVPdx4kOs1SyM2g3T8O1IP104mKXBJ5MuwrM8jp8Tvl7CHi/ylkX2lqiWdkA89+iq7OTneavppoecN4BojwHxKLghl9ewAeQ9KAcOXmyb9f6g273k+E31WK9KgeEukqnFrJDaItwWqbK+Aw9My4os9xK/Dyq939kDhnkGLFdFeAqdgITzOlHOJur4DfaljFi2njdr3aOOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sd2DaqAF9f6XFL8sOviCRMjMgOpzvTQI9x334caVHiISvubN7jfqV+D4+skC+aJbY4R/j36Lq52tLbVkXYllApFLuGS1pwNZSXgR6U0EwCieXPpx+w5PyIPtws6QvbtjQTbAzFWbne2Gak742NiUd70PcL4XomoxYe58mKjBJQPPzJJD1mNFTHjcIDWA65ROhLXGddol3k/bZbkS4Il0kvz5grzyr4iL/aMvyNE6NTs09964+CVnhY3p2R5

Siddharth said
I do not understand why there has been an explosion of interest in HoTT, when it seems to me that CIC can do whatever HoTT can?

One of the more interesting features of HoTT is that it allows to do synthetic homotopy theory.

Is possible to do synthetic homotopy theory in CiC without introducing new axioms, just like it is done in HoTT? Are there some essential differences?

[Coq-Club] HoTT ideas already present in CIC?, Siddharth Bhat, 05/26/2018
- Re: [Coq-Club] HoTT ideas already present in CIC?, Jason -Zhong Sheng- Hu, 05/26/2018
  - Re: [Coq-Club] HoTT ideas already present in CIC?, Siddharth Bhat, 05/27/2018
    - Re: [Coq-Club] HoTT ideas already present in CIC?, Éric Tanter, 05/27/2018
      - Re: [Coq-Club] HoTT ideas already present in CIC?, Éric Tanter, 05/27/2018
        
        Re: [Coq-Club] HoTT ideas already present in CIC?, José Manuel Rodriguez Caballero, 05/27/2018
        
        Re: [Coq-Club] HoTT ideas already present in CIC?, Siddharth Bhat, 05/27/2018
        
        Re: [Coq-Club] HoTT ideas already present in CIC?, José Manuel Rodriguez Caballero, 05/27/2018
- Re: [Coq-Club] HoTT ideas already present in CIC?, Thorsten Altenkirch, 05/27/2018