The Coq mailing list

[Éric Tanter <etanter AT dcc.uchile.cl>]

sorry, forgot the link of the preprint: https://hal.inria.fr/hal-01559073

— Éric

On May 27, 2018, at 9:39 AM, Éric Tanter <etanter AT dcc.uchile.cl> wrote:

Hi Siddharth,

Regarding part 2, you might be interested in our work on Equivalences for Free (to appear at ICFP’18):

Abstract : Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. We present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. Our approach handles both type and term dependency. We study how to maximize the effectiveness of these transports in terms of computational behavior, and identify a fragment useful for certified programming on which univalent transport is guaranteed to be effective.

HTH,

— Éric

On May 27, 2018, at 9:03 AM, Siddharth Bhat <siddu.druid AT gmail.com> wrote:

I see, interesting. Could you provide me a reference to read more about impredicavity of CIC? 

And, do you have any thoughts on part 2, regarding univalance and why it is interesting?

Thanks

Siddharth

On Sun 27 May, 2018, 01:03 Jason -Zhong Sheng- Hu, <fdhzs2010 AT hotmail.com> wrote:

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!

--

Sending this from my phone, please excuse any typos!