(guest post by Jesse McKeown)
A short narative of a brief confusion, leading to yet-another-reason-to-think-about-univalence, after which the Author exposes his vaguer thinking to derision.
The Back-story
In the comments to Abstract Types with Isomorphic Types, Dan Licata mentioned O(bservational)TT, originating in works of McBride, with Altenkirche, McKinna… One of the initially-strange features therein is a so-called "heterogeneous equality" type, which from my very cursory reading I see has something to do with coercing along equivalences. Of course, this piqued my curiosity and a short-while later I happened upon this book about using coq as a practical program verification assistant, by way of this section of the chapter "Equality".
The Types
A heterogeneous equality type is defined in standard Coq (in the library Coq.Logic.JMeq) more-or-less by
Inductive JMeq { A : Type } (a : A) : forall { B : Type }, B -> Type :=
jm_refl : JMeq a a.Andrej Bauer’s modified "hoq" omits this library, for what turn out to be very sensible reasons (that is, the file isn’t even present to tempt us); nonetheless, I was curious to see what would happen if one tried to reason directly about this sort of equality instead of the HoTT-usual sort; in my case, foolishly trying to hand-edit the Paths library to replace paths with this JMeq. The surprising result was a flurry of Universe.Inconsistency (warnings) as soon as I tried to prove the left- and right-unit laws. This was when I actually started looking for written things about heterogeneous equality types in Coq on the internet, landing on Chlipala’s book. He makes what seemed a curious remark about a possible axiom JMeq_eq of type
JMeq_eq_axiom := forall {A : Type} (x y : A), JMeq x y -> x = y .saying
It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of match annotations.
Particularly, the second sentence struck me as odd, because the incompleteness of an axiomatic theory has nothing to do with the concrete syntax you use for talking about that theory — that would mean your metalanguage was inadequate, not that the theory itself was incomplete. What is actually going on is that an inhabitant of JMeq_eq_axiom is an anti-Univalence-axiom: it says that the Universe of types is totally-disconnected. It does not say much of anything about homotopy within types generically.
Heterogeneous Equality with Univalence
To clarify the preceding, if one attends to what is deliberately obscured by the implicit arguments of JMeq 1, you will see that "heterogeneous equality" is really "equality of pointed types". And so, some code.
Definition ptdType := { A : Type & A }.
Definition unptd : ptdType -> Type := pr1.
Definition basept : forall A' : ptdType, unptd A' := pr2.
Definition at_home { A : Type } (a : A) : ptdType := existT ( fun x => x) A a.
Notation "[ a ]" := (at_home a).Of course, anyone who is interested in homotopy theory should think about pointed spaces from time to time, if only because of the hypotheses of Brown’s representability theorem. Two easy lemmas about basept and at_home; we only need one of them here; we’d probably want the other if proving equivalences in the other order below.
(* a beta *)
Definition b_a_b { A : Type } (a : A) : basept [a] = a.
auto.
Defined.
(* an eta *)
Definition a_b_a (w : ptdType) : [ basept w ] = w.
destruct w.
auto.
Defined.Mike, in email, reminded me that these are just eta and beta (or η and β, if you like), but I’m leaving these names in for now, because these are the sorts of observations that confuse me. And now we can really begin to consider what it means to identify two pointed types.
Lemma jme_to_ptEq : forall { A B } (a : A)(b : B), JMeq a b -> [a] = [b].
Proof.
intros.
induction X.
auto. (* "apply idpath" *)
Defined.
Lemma ptEq_to_jme : forall w v, w = v -> JMeq (basept w) (basept v).
Proof.
intros.
induction X.
apply jm_refl.
Defined. Really, that bit was quite trivial, which is why the next bit is so easy: these are (more-or-less) inverse equivalences.
Lemma ptdEquiv : forall w v, hequiv (w = v) (JMeq (basept w) (basept v)).
Proof.
intros. (* w v *)
exists (ptEq_to_jme w v)
(fun y =>
! a_b_a w @ (jme_to_ptEq (basept w) (basept v) y) @ a_b_a v).
(* proving hequiv_section *)
intros. (* y : JMeq (basept w) (basept v) *)
destruct w as [W w].
destruct v as [V v]. simpl in *. (* now, y : JMeq w v *)
induction y.
compute. auto.
(* hequiv_section done! now proving hequiv_retraction *)
intros. (* x : w = v *)
induction x.
destruct w.
auto. (* that's all! *)
Defined.There, that was easy. The other side is even easier, now:
Definition JMEquiv : forall {A B} (a : A) (b : B), hequiv ([a] = [b]) (JMeq a b) :=
fun A B (a : A)(b : B) => ptdEquiv [a] [b].-
You might say "obscured by me" because standard Coq defers this obscurantism to its local notation "==". It’s still there, just the same. (back)
Homotopy Type Theory 
Nice! Let me carry that a bit further. You’ve shown that JMeq a b is equivalent to [a]=[b], or in more explicit notation (A,a) = (B,b). But by the standard identification of identity types of Σ-types (called something like total_path_equiv in the HoTT library), an inhabitant of (A,a) = (B,b) consists of an equality p : A=B together with an equality transport p a = b. Univalence says that even if A and B are definitionally equal, p may not be reflexivity; thus transport p a = b is not the same as a = b.
This is especially timely, because the other day several of us were discussing the various possible ways to represent “dependent identity types” such as occur in the elimination rules for HITs. Given a type A and a dependent type
Type, elements 
and an equality 
, and elements 
and 
, one wants a type of “equalities between 
and 
lying over p“, which might be written as 
.
The definition we’ve been using so far is
. It’s also possible to define 
directly as an inductive type:
Type) :
:A) (p:
) (
:B 
) (
:B 
), Type :=
A 
B 
Type :=
, and 
as above, we would consider
) (B 
) (map B p) 
Inductive dep_eq {A:Type} (B:A
forall (
| dep_refl : forall (a:A) (b:B a), dep_eq B a a (refl a) b b.
But a third possibility is a sort of heterogeneous equality parametrized by equalities between types, something like
Inductive JM_eq' : forall (A B:Type), (A=B)
| JM_refl' : forall (A:Type) (a:A), JM_eq' A A (refl A) a a.
Then given
JM_eq' (B
Here a maybe a somewhat off-topic comment, but expanding on the above side-remark that
“anyone who is interested in homotopy theory should think about pointed spaces from time to time”:
Of particular interest are pointed _connected_ types: pointed connected types are equivalently oo-groups (whereas unpointed connected types are oo-gerbes…) and HoTT in the context of a pointed connected type is the representation theory of the oo-group of loops of that type. A type depending on a pointed connected type is an action/representation of that oo-group; the dependent product over it is the invariants of the representation; and the dependent sum over it is the quotient of the representation. And since all this is automatically homotopy-theoretic, those invariants are actually the group cohomology with coefficients in that representation, and so forth.
It seems to me that the power of this identification
HoTT in context of pointed connected type homotopy group representation theory
has not been widely exploited yet. For HoTT theorist it might be easy to use this to make some genuine contrinution to homotopy theory. In my experience traditional homotopy theorists are in fact not very familiar with the full generality of the notion of what they call “strong homotopy representations” or (worse but increasingly in some circles) “representations up to homotopy “. The reason is, I think, that it becomes transparent only when thought of dependent type-theoretically.
I know that for instance homotopy theorist Jim Stasheff has been trying to get an overview of the basics of “strong homotopy representation theory”. Recently he posted to the nForum saying that he is now beginning to write up some “history” on it: http://nforum.mathforge.org/discussion/2376/homotopy-actions/?Focus=37024#Comment_37024
Of course, strong homotopy representations also go by the name of “parametrized homotopy theory” over a pointed connected space. One might argue that that point of view is making use of some of the same advantages of the dependent-type-theory perspective, inside of classical homotopy theory.
True, thanks, good point.
On the other hand, in May-Sugurdsson’s “Parameterized homotoy theory” (for other readers: available at http://www.math.uiuc.edu/K-theory/0716/MaySig.pdf) this potential point of view is not really made explicit. (Or is it? I haven’t read through all of it.) Where group actions appear they are implemented in the traditional fashion. Notably part III is about homotopy theory over a base that _in addition_ is equipped with a group action formulated in the traditional way. So it seems to me that May-Sigurdsson provide some crucial ingredients for studying higher representation theory by means of slicing, but it’s not developed there in any way (as far as I can see, at least).
Elsewhere there are books and articles that try to deal piecemeal and with some effort to come to terms with formulating representation theory of 2-groups. This is immediately subsumed and generalized by simply going to HoTT in the context of a pointed connected type.
And then there is much more to be found there, which I haven’t mentioned above yet, by looking at relative base change. For instance dependent sum along a morphism of oo-groups = pointed connected types is the induced-representation functor. The dependent product is coinduction of representations.
Currently we are writing in article where we show that for
a morphism of pointed connected types, the canonical function
for any $G$-representation $E$ captures the group extensions that in symplectic geometry are known as “quantomorphism groups”. Plenty of structure to be found there.
So in summary my point is that there is lots of interesting and low-hanging-fruit to be picked by simply understanding HoTT in the context of pointed connected types as oo-representation theory.
The things that May and Sigurdsson call group actions are not actually strong homotopy representations in this sense, because they treat them from the perspective of traditional equivariant homotopy theory, which cares about fixed-point sets. Those sort of spaces are best understood from a homotopical point of view as diagrams on the orbit category of a group.
I was thinking only of the case where their “group of equivariance” is trivial. Just take the base space to be the classifying space of your group. They don’t use the language of group actions, but I think if you translate everything they say into that language then you’ll find a lot of good stuff. And it’s the same translation as when you think of the context of a pointed connected type in DTT.
Yes, I understand, that’s what I meant, too. I am just thinking that it’s a non-trivial conceptual step from having the tools for working relative over a base to realizing that this is related to representation theory. The same statement also applies to the vast classical literature on universal V-fibrations in homotopy theory. These are objects in the slice of ooGrpd over a pointed connected type and classical tools allow one in principle to go ahead and study oo-representation theory this way (the universal V-fibration identifies then with the canonical Aut(V)-action, and so forth). But I am not aware of a lot of literature that actually adopts this point of view and then actually takes advantage of it.
It’s time to take full advantage of this, and HoTT is a natural tool for doing so. That’s all I am saying.
An almost-totally-irrelevant side note, that “JM” in the preceding stands for “John Major”, not something else you might think of, and I suppose we should ask Conor what that is all about.
Quoting from Conor’s thesis, section 5.1.3:
“It is now time to reveal the definition of ≃, the ‘John Major’ equality relation. (Footnote 2: John Major was the last ever leader of the Conservative Party to be Prime Minister (1990 to 1997) of the United Kingdom, in case he has slipped your mind.) John Major’s ‘classless society’ widened people’s aspirations to equality, but also the gap between rich and poor. After all, aspiring to be equal to others than oneself is the politics of envy. In much the same way, ≃ forms equations between members of any type, but they cannot be treated as equals (ie substituted) unless they are of the same type. Just as before, each thing is only equal to itself.”
(Of course, Conor’s prediction in the footnote was refuted with the election of David Cameron in 2010.)
It’s a shame that partisan politics of a particular country have been snuck into the naming of an interesting mathematical object. Maybe we can agree to just call this “heterogeneous equality”, which is also a more descriptive name.
And also, strip Connor of his PhD since his thesis contains factual errors.
I don’t know, it seems that this is all in good fun. I really appreciate the humanisation of abstract mathematics in the way Conor does.
Aye!
I think so do Andrej and the rest; and it comes out differently with them.
I’d like to point out that OTT’s equality is not JMeq though: rather than bundling a path between the types it asks for one.
So it’s more like the following
OTTeq : (A B : Type) (x : A) (y : B) -> Type
OTTeq A B x y = forall (p : A = B), transport p a = b
Which I believe is even less sensical from a HoTT perspective, because if that p can be any isomorphism one can’t even prove OTTeq Bool Bool true true
I should hasten to add that I’m not critiquing OTT or the use of highlighting particular Inductives; hmmm… that does still look like a strange thing to highlight — a term of this OTTeq would say that the *tautological fibration* over Type on the component of Bool were trivial… you could still have, for instance, an equivalence ( (Bool = Bool ) (Bool Bool) ), but you couldn’t have that equivalence realized by path_to_equiv. It would be weird indeed!
But! You could have that trivially-fibered equivalence at one level of Type, and find the usual Univalence at a higher level… one of the things I left out of this note was a vague wondering about whether one could ask for Univalence only “in the limit”, but never mind that now. I’m rambling again.
I believe one way to embed OTTeq in a system with Univalence would be to have an hset U (for Universe) equipped with an interpretation function T : U -> Type and then define the equality like so
OTTeq : (A B : U) (x : T A) (y : T B) -> Type
OTTeq A B x y = forall (p : A = B), transport (map T p) x = y
and then we’d have to decide how to populate this U type, it might even cover the whole hierarchy of Type unless paradoxes are lurking beneath.
I don’t understand; how is that any more univalent? It looks like the same equality from your first comment.
A and B are elements of U not Type, intuitively they are just syntax for types rather than types themselves, so A = B is contractible and a stronger assertion than T A = T B, hence assuming ‘Bool’ : U; and T ‘Bool’ = Bool we can indeed prove OTTeq ‘Bool’ ‘Bool’ true true, because we know the only inhabitant of ‘Bool’ = ‘Bool’ is refl.
So I guess it’d be a way to consistently reason “non-univalently” within an univalent theory.
Oh, I misunderstood what you were saying. Yes, that makes sense: you can have non-univalent “universe objects” in a univalent theory.