The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

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!