Why are equivalences so hard to prove?

[Alizter]

Checking out Spheres.v you can see a proof of isequiv_Sph2_to_S2. It is really long and quite unreadable.

I was trying to prove the following on my own:

Lemma susp_equiv_coeq {X : Type} : Susp X <~> Coeq (fun _ : X => true) (fun _ => false).

And I get the same problem. The complexity blows up whenever I try to give sections.

One thing I could imagine helping is if "compute" could use the eliminations for HITs, however that doesn't seem likely.

Is there anything I can do to help simplify what I am doing here? Can we give a simpler proof of isequiv_Sph2_to_S2?

[mikeshulman]

It could be that that proof could be simplified using cubical methods as in Licata-Brunerie. I haven't thought about it. One would presumably need to (re)state the elimination rules for the relevant HITs in a more cubical style.

[Alizter]

Actually I think if we used cubical machinary for many of the indcution princples of higher inductive types we would have a much easier time using them. I'll see if I can have a go changing S2_ind to use the cubical stuff and see what happens.

[Alizter]

So I have had a go here. This doesn't really work however. I've only really made a mess of it.

The problem with restating in a more cubical style is that its a lot easier said then done. There is obviously a lack of helpful lemmas which will take a bit of time to write out. Overall there is much more needing to be done to get any use out of cubical stuff.

One thing I am been thinking about is Mortberg and friends' cubical type theory. They seem to have quite an easy time messing around with HITs and path algebra. There is of course the question of, do results using their funny univalence construction translate well into book HoTT.

It seems to me that cubical type theory adds two things to the table: Licata-Brunerie style cubical reasoning everywhere and constructive univalence. Even the HoTT-agda formalisation doesn't use LB cubical methods everywhere, and from what I am seen of cubical-agda, LB does simply a lot.

[mikeshulman]

Well, there's not much point in ruminating about cubical type theory if the goal is to formalize things in this library, which uses Coq and Book HoTT. Personally I think there is still a lot to be said for Book HoTT relative to the current generation of cubical type theories. It certainly makes sense that there will be a lot of missing lemmas in order to consistently use LB cubical methods in a library like this one that wasn't developed for them from the outset. Perhaps a better approach would be to work on a branch of the whole library that ports all the basic lemmas to LB cubical style, throughout the Basics and Types directory, and then if & when it's finished consider replacing the main library with it. However, I think it's true that LB cubes don't solve all problems, and may introduce some new ones, e.g. you may sometimes have to do a lot of passing back and forth between non-definitionally-equal notions of "dependent path".

[Alizter]

Can you elaborate on the last point? Which definitions of "dependent path" mgiht not be definitionally equal?

[Alizter]

I wonder if we can make dpath definitionally equal to p # x = y would this solve some problems? Perhaps allowing us not to rewrite Basics?

[mikeshulman]

Yes, that's exactly it; the DPath here isn't definitionally equal to p # x = y. And you're right, if the plan were to integrate better with the rest of the library, then probably it would simplify a lot of things to just define DPath to be p # x = y.

[Alizter]

Do you know of any other references other than LB that talk about the use of cubical constructs in HoTT? I'm interested if anybody has studied HITs with only cubical constructors, as I imagine it would make it easier to write down an induction principle for.

How can we make coq recognise that things like DPath and DSquare should reduce to their non-dependent counterparts when the type family is constant. If we define DPath as I said above then this might happen automatically but I can't seem to do it for DSquare (probably because its the wrong definition).

[spitters]

https://arxiv.org/abs/1802.01170 On Higher Inductive Types in Cubical Type Theory

On Mon, Jan 14, 2019 at 12:05 PM Alizter notifications@github.com wrote:

Do you know of any other references other than LB that talk about the use of cubical constructs in HoTT? I'm interested if anybody has studied HITs with only cubical constructors, as I imagine it would make it easier to write down an induction principle for.

How can we make coq recognise that things like DPath and DSquare should reduce to their non-dependent counterparts when the type family is constant. If we define DPath as I said above then this might happen automatically but I can't seem to do it for DSquare (probably because its the wrong definition).

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HoTT/HoTT/issues/983#issuecomment-453968473, or mute the thread https://github.com/notifications/unsubscribe-auth/AAM2zkJzLfNR4VcfiO27K3E5Km8JN618ks5vDGRjgaJpZM4Z8YtU .

[Alizter]

@spitters

But this is about cubical type theory. I am really asking about using cubical constructs in book hott. "cubical type theory" is different because it has glue types which give it a constructive univalence etc.

Evan Cavallo had a paper on cohomology a bit back. In that he discussed cubical methods in HoTT like in LB. I'm looking for something along the lines of that.

[mikeshulman]

It's not possible in Book HoTT to define dependent paths generically for all types in a way that will reduce definitionally to non-dependent paths for a constant type family. This is one of the big advantages of cubical type theory. A while back I had an idea to partially fake this in Coq using typeclasses, but never pursued it further.

[Alizter]

@mikeshulman Do you have any more information on faking it, or is it a dead end?

[mikeshulman]

I don't know whether it's a dead end; as I said, I never pursued it further to find out.

[Alizter]

How can typeclasses help you partially fake this?

[mikeshulman]

Define a typeclass like

Class HasDPaths (B : A -> Type) :=
| dpath : forall (a1 a2 : A) (b1 : B a1) (b2 : B a2) (p : a1 = a2), Type
| <some induction principle>

and then for every type family you want to have definitionally-computing dpaths (including constant type families), define an instance of this typeclass, plus a "catch-all" instance of lowest priority that gives the default definition (e.g. p # x = y) for an arbitrary type family. The point is that you can't define things inside type theory "by induction over type constructors", but you sort of can do that at proof-assistant level because typeclasses can dispatch on the syntactic form of a term (even more finely than definitional equality).