The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

I'm trying below to answer some of the questions from last week
discussion which were not yet addressed. This is long and a bit
technical but I hope it can be of interest for some readers of the
list. The quick summary is:

I Infinity-groupoid structure and univalence in CIC
II More in HoTT than in CIC?
III Other questions: impredicativity, synthetic homotopy

Best,

Hugo

----------------------------------------------------------------------
I Infinity-groupoid structure and univalence in CIC

On Sun, May 27, 2018 at 12:30:03AM +0530, Siddharth Bhat wrote:
> 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?

The infinity-groupoid structure of types comes from the presence of
Martin-Löf's identity type, so it is present in CIC, even though the
equivalent of the identity type in CIC ("eq") has type Prop in CIC.

The corresponding infinity-groupoid would be degenerate in the
presence of proof-irrelevance (one inhabitant in each Hom), but it can
a priori be as big as a model of Coq's Prop can be, which, due to
impredicativity, would typically constrain each type in Prop to be a
set of terms (logical relations or reducibility candidates) as in a
realisability model.

[Note: I'm not a specialist of Coq models in the sense that I did
not strongly put my hands in building such models for Coq; I'm only
talking here as an informed outsider.]

Then, formulating univalence in Coq's Set is certainly consistent
because Coq's Prop and Coq's Set can both be interpreted the same, as
a set of reducibility candidates. So Prop shall be big enough to
contain all isomorphisms that can be built between types in Set.

On the other side, if univalence is formulated in a higher universe,
say in Coq's Type(1), this is suspectingly inconsistent. At least, it
would be, if we arrive to build an equivalence between two types of
Coq's Type(1) which is not interpretable in the larger model we know
how to build for Coq's Prop. Of course, this equivalence would have to
involve Coq's Set since otherwise, we are back to the question of
setting univalence in Set. I don't know if someone on the list knows
the answer to this question (typical names I know who may be able to
answer this kind of question are Nicolai Kraus and Christian Sattler).

At least, what I can say is that I'm not aware of a model of Coq with
univalence in Type(1) which would be compatible with having eq in
Coq's Prop.

For this latter reason, Coq has an option -indices-matter which allows
to define "eq" in Coq's Type hierarchy whenever its arguments are
liable to have a non-trivial infinity-groupoid structure. With such
definition of equality, univalence can be stated and the topological
model applies, interpreting e.g. Prop as hProp with resizing (though,
maybe, other interpretations of Prop based on propositional truncation
are also possible).

An alternative direction would be not to interpret Coq's Type(i) as
HoTT's Type(i) but rather as HoTT's hSet(i) (the level of hSets in
HoTT's Type(i)). We could then add a new Coq universe, say Univ(i)
which would correspond to HoTT's Type(i) and state univalence in
Univ(i). By doing so, we would preserve the current organization of
sorts of Coq, since "eq" on hSet(i) is indeed in hProp (I identify
here all hProp(i) with hProp(0)).

> 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?

See indeed answers from Eric and Thorsten.


II More in HoTT than in CIC?

> 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?

Technically, HoTT in itself, as a logic, is not fundamentally
different from CIC or from Agda's logic. However, the ideas behind
HoTT are going much further than what the logicians were able to say
about Martin-Löf's type theory before the emergence of these
ideas. This includes the type-as-space/type-as-infinity-groupoid
correspondence discovered in the 2000's by Awodey, Warren, Voevodsky, ...,
the invention of Higher Inductive Types by Bauer, Lumsdaine, Shulman,
the ability to use Martin-Löf's for a synthetic approach of homotopy
theory, the development by Voevodsky of univalence as a mathematically
important and natural notion of extensionality on types (especially in
a context where set theory is not able to state such kind of universe
extensionality), as well as a whole bunch of related concepts, such as
Voevodsky's h-levels.

For instance, before the HoTT ideas emerge, the status of the
awareness of the infinity-groupoid structure of types was limited to
the level of 1-groupoid as developed by Hofmann and Streicher, and,
even if a version of univalence at level Type(1) was already stated in
Hofmann and Streicher, it was not considered at that time as something
fundamental from the mathematical point of view. (See the introduction
of the HoTT Book (https://homotopytypetheory.org/book/) for more.)

So, shortly, HoTT comes with a lot of new ideas, but, technically,
these ideas are indeed already expressible in the usual context of
type theory. After a 50 years old proofs-as-programs correspondence
which has still not delivered all its fruits (e.g. wrt to side
effects, or in fully programming with dependent types), HoTT is a new
historical example of a conceptual convergence of structures between
different domains, now including logic, computer science, category
theory and homotopy theory. Moreover, by crossing the ideas specific
to each discipline, this convergence itself triggers various new open
problems which shall feed the research for probably many years to come
(e.g. what it means to compute with univalence, to compute with the
axiom of choice, to have a type-as-infinity-category correspondence,
to reason up to modalities, and so on).


III Other questions: impredicativity, synthetic homotopy

On Sat, May 26, 2018 at 07:32:23PM +0000, Jason-Zhong Sheng-Hu wrote:
> 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.

I don't know what would people at the heart of HoTT like Andrej Bauer
or Michael Schulman say about that, but there is a notion of resizing
rule in the context of HoTT which makes hProp impredicative. So, my
perception is that HoTT is not tight to only predicativity in general
but rather that they are some people which feel comfortable with
impredicativity and other which prefer to avoid impredicativity.

> With the presence of impredicativity, you cannot obtain proof
> relevance; in the case otherwise, you will get into Russell's paradox.

See above: impredicativity in itself does not imply proof-irrelevance,
but impredicative sorts have rather constrained interpretations,
typically realizability-based models (see Reynolds' "polymorphism is
not set-theoretic").

On Sun, May 27, 2018 at 05:06:45PM +0200, José Manuel Rodriguez Caballero 
wrote:
> Is possible to do synthetic homotopy theory in CiC without introducing new
> axioms, just like it is done in HoTT?

Having met you at the Coq implementor workshop last week, you
clarified to me that your question was "how much can we do synthetic
homotopy theory without univalence and higher inductive types". The
answer is that I don't know precisely, but some people on the list
certainly have a better idea of what is possible to do. Otherwise,
answers can certainly be found by browsing one of those formal
development of synthetic homotopy:

- https://github.com/mortberg/cubicaltt
- https://github.com/HoTT/HoTT-Agda
- https://github.com/HoTT/HoTT/ (HoTT-Coq)
- http://florisvandoorn.com/talks/MURI2016.pdf (HoTT in Lean)
- https://github.com/UniMath/UniMath (UniMath in Coq)

On Sun, May 27, 2018 at 08:30:50PM +0000, Thorsten Altenkirch wrote:
> 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.
> 
> 
> 
>