The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Siddharth,

To the best of my understanding, for the first point, the equality in Coq cannot be used, as it's defined to be impredicative, while HoTT is really predicative. With the presence of impredicativity, you cannot obtain proof relevance; in the case otherwise, you will get into Russell's paradox. Essentially, what's stopping you from going to ?A : Prop is that any Prop is necessarily opaque. To achieve infinite groupoid, you will need an infinite hierarchy of universes to state that, which says eq needs to live in Type instead.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Siddharth Bhat <siddu.druid AT gmail.com>
Sent: May 26, 2018 3:00:03 PM
To: Coq-Club Club
Subject: [Coq-Club] HoTT ideas already present in CIC?

 

Hello all,

I've been trying to understand the philosophy of HoTT, and the distinctions it presents with CIC.

So, from what I can tell, the major difference between the two seems to be:

1. The infinity-groupoid structure.

2. The univalence axiom.

Regarding #1, Why not construct this "tower of equalities" within CIC? I understand that the regular eq type has the signature:

eq

     : ?A -> ?A -> Prop

where

?A : [ |- Type] 

But what stops us from setting

?A : [ |- Prop]

and recovering the "infinity groupoid? As long as we do not have proof irrelevance, the tower should not collapse, right?

2. Univalence:

Let me first sketch out what I understand of Univalence, to make sure I have not missed something with the definition itself. Univalence talks about two things:

a. Equality, which is a type with one constructor refl, which models Leibniz equality.

b. Equivalence, which is a constructive bijection between two objects.

Univalence states that "equality is equivalent to equivalence". The forward direction (equality -> equivalence) is clear (if a = b,  use id as the bijection between a and b). The backward (equivalence -> equality) is taken to be the axiom which we cannot prove within HoTT. Roughly, the philosophy seems to say that "equivalent objects are equal".

In Coq/CIC, do we not already sort of take this persective when using Setoids? essentially, we are saying that "we do not care about true equality", but we are happy working with stuff "upto equivalence". Is this not exactly what Univalence is trying to do? I understand that CIC does not let you convert  from equivalence to equality, but does that really matter?

What am I missing here, in my understanding of HoTT? 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?

Thanks,

~Siddharth

--

Sending this from my phone, please excuse any typos!