The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Siddarth,

indeed in type theory the tower of equalities gives rise to an omega-groupoid (this was proven by Peter Lumsdaine in his PhD). 

However, equality in intensional type theory reflects definitional equality, that is in the empty context definitional equality and propositional equality (or better the equality type) coincide. So in particular functional extensionality and all forms of univalence (even propositional extensionality: tow propositions are equal iff they are logically equivalent) fail. Intensional type theory seems rather cruel in so far that it imposes a lot of discipline (extensionally equivalent objects cannot be distinguished) but it never pays back (extensionally equivalent objects are not equal).

The view in HoTT is that every type comes with its equality, I.e. every type is considered as an omega groupoid. This view allows us to adopt an extensional view of equality. Your analogy with setoids is correct, basically omega groupoids are setoids on steroids. The equality type is not really an inductive definition but an interface to access this tower of equality.

I think the attempt to overcome the weaknesses of intensional type theory with setoids is doomed, it leads to a setoid hell glowing up even simple constructions. Also setoids do not introduce a real abstraction barrier, we can still access the underlying representation. It seems preferable to rather work in a type theory of setoids, which is what we have tried to do (1st in my LICS paper in '99 and then with the development of OTT). 

HoTT goes further and I haven't seen anybody suggestion that we could use higher groupoids explicitly in intensional type theory. I guess setoid hell is nothing compared to this.

The problem is basically solved due to the work of Thierry Coquand et al on cubical type theory. The way to go for systems like Coq, Agda, Idris,… is to follow the lead and implement a version of cubical type theory. In cubical type theory equality are paths, I.e. functions from a generic interval (pre-)type into a type. The fundamental concepts of the intensional equality type (reflexivity, the eliminator aka J aka path induction) are no longer primitive but derivable, in the case of reflexivity by the constant function and the eliminator is derivable from the Kan-fillers (compose terms). They are no longer primitive and the computational rule for the equality type doesn't hold in cubical type theory (this can be fixed but I have some doubts wether this is a good idea).

Thorsten

From: <coq-club-request AT inria.fr> on behalf of Siddharth Bhat <siddu.druid AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Saturday, 26 May 2018 at 20:00
To: Coq-Club Club <coq-club AT inria.fr>
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!

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.