Bundled vs unbundled

[mikeshulman]

trafficstars

I feel like the main thing missing from Coq to make passing between bundled and unbundled structures easy is the ability to automatically coerce an unbundled object to a bundled one by invoking a typeclass search. That is, we can declare a coercion pType >-> Type and an IsPointed instance for it, so that elements of pType can be automatically unbundled. But we should also be able to use an element of Type as a pType if an IsPointed instance for it can be found by typeclass search. If we had that, then the bundled and unbundled versions would be silently isomorphic.

It seems to me that something like that could be implemented in a more flexible metalanguage such as Andromeda. But in Coq, we can still do something like the hottclasses:

Class Cast A B := cast: A -> B.
Arguments cast _ _ {Cast} _.
Notation "' x" := (cast _ _ x) (at level 20) : mc_scope.
Typeclasses Transparent Cast.

This doesn't yet do a typeclass search, but what if we had something like

Class Cast {A} B (x : A) := cast : B.
Notation "' x" := (@cast _ _ x) (at level 20).

Could we then do something like

Global Instance equiv_cast A B (f : A -> B) `{IsEquiv A B f}
  : Cast (A <~> B) f
  := BuildEquiv f _.

and then write ' f to make any function into an equivalence by invoking typeclass search for an IsEquiv instance? If so, this might simplify our lives by eliminating the need for lots of equiv_ lemmas (though I suppose having to go through typeclass search might slow things down).

[mikeshulman]

Here is another vague thought: it seems to me that unbundled structures work well when the carrier belongs to a positive type (including the universe), since then typeclass search is very syntax-directed. E.g. we can infer IsTrunc instances very well since we have parametric instances for all the basic type formers. Whereas bundled structures seem to work better when the carrier belongs to a negative type, such as a function type. E.g. a general function is usually defined as a lambda-abstraction, and typeclass inference has a hard time breaking this down into pieces that could be assembled via parametric instances. Hence we don't make a whole lot of use of parametric IsEquiv instances, instead we often reason directly on the bundled equivalences since they allow us to specify exactly how a function that is an equivalence is put together (that not being obvious from its syntax, unlike how a type that is an n-type is put together). This is probably an overgeneralization but I feel like there is something there.

[Alizter]

Which kinds of bundled objects would this apply to however? Take for example doubly pointed types. Then there would be two different instances of IsPointed floating around. When coq goes to bundle them back up how would it know where to put which instance?

If we were to carry out something like this, we would have to somehow prove that there is a one-to-one correspondence with unbundled and bundled things.

[fpvandoorn]

This comment is also related to #1211.

My experience with equivalences in Lean is that type-class inference is too slow and (at least in the case of Lean) too brittle. For this reason during development I slowly moved to the direction of using bundled equivalences whenever possible, and almost never use unbundled equivalences (and the same is true for group homomorphisms and any other type class on functions). There are some cases where I still used unbundled equivalences, for example to formulate universal properties. These are usually formulated by stating that some specific (universal) map is an equivalence. When proving universal properties, usually the first lemma I applied was the lemma stating that if e : A <~> B and e == f then IsEquiv f (in which case I'm working with bundled equivalences again). When using universal properties, I just used it as a bundled equivalence. This limits the type class problems for equivalences to almost 0. If I would build a library from scratch, I would try not even making IsEquiv a class.

There are some patterns of reasoning that are a little trickier with bundled equivalences. For example, if for unbundled equivalences you would apply the lemma IsEquiv g -> IsEquiv (g o f) -> IsEquiv f for bundled equivalences I would have g : B <~> C and gf : A <~>C and then use g ^-1 oE gf and show that this map is homotopic to the function f : A -> B I want to prove to be an equivalence. This is slightly more awkward than the unbundled lemma. However, usually the map from A -> C is not definitionally equal to g o f, but only homotopic to it, and then you need an additional lemma in the unbundled case.

In Coq I've also noticed that type class inference for equivalences is sometimes very slow. One example is demonstrated in #1204, another one I noticed is the following. Sometimes, when I have f : A <~> B and I write f ^-1, type class inference can still take multiple seconds to find the single instance equiv_isequiv. It is instantaneous when I write f ^-1 % equiv (e.g. here https://github.com/mikeshulman/HoTT/blob/82a893ed7464424fe346dd30f1e832d33f1b7080/theories/Pointed/Core.v#L329).

My suggestions:

• Formulate all lemmas about equivalences (also) using bundled equivalences, and make those the "default" ones (e.g. if the lemma using unbundled and bundled equivalences would want the same name, add a prime to the lemma using the unbundled equivalence)
• Encourage bundled equivalences via notation. By default ^-1 and oE should take bundled equivalences as arguments.
• (Slowly) go through the library and use the lemmas formulated with bundled equivalences instead of the ones with unbundled equivalences.

If these suggestions are followed, then bundling up an unbundled equivalence shouldn't need to happen very often, because the equivalences you want to use are already bundled up. I think that if you rely on type-class inference to promote a function to a bundled equivalence, you will regularly run into performance issues.

Note: this argument doesn't really work on type-classes on the universe (like IsTrunc or Pointed), although in the case of pointed type, we also almost exclusively used the bundled version. For IsTrunc we usually used type-class inference.

[mikeshulman]

Yes, I think I'm on board with that proposal now. It's amusing that while in category theory it's important to formulate universal properties as some particular map being an equivalence, rather than the mere existence of an equivalence, whereas in a proof-relevant proof assistant that information can be carried by the computational behavior of the specified equivalence.

the lemma stating that if e : A <~> B and e == f then IsEquiv f

FWIW, I defined that lemma in #1207 as isequiv_homotopic'.

usually the map from A -> C is not definitionally equal to g o f, but only homotopic to it, and then you need an additional lemma in the unbundled case.

But this seems like a common enough pattern that we could combine the two lemmas: forall (g : B <~> C) (gf : A <~> C), (g o f == gf) -> IsEquiv f.

[fpvandoorn]

the lemma stating that if e : A <~> B and e == f then IsEquiv f

FWIW, I defined that lemma in #1207 as isequiv_homotopic'.

Ah good, now we just need to move the prime ;-)

But this seems like a common enough pattern that we could combine the two lemmas: forall (g : B <~> C) (gf : A <~> C), (g o f == gf) -> IsEquiv f.

Yes, that sounds useful.

[spitters]

There is an Emacs plugin that does this for agda. I wonder how hard it is to port this to Coq. https://alhassy.github.io/next-700-module-systems/

A more principled approach would probably use meta-coq.

On Thu, Dec 26, 2019 at 12:22 PM Mike Shulman [email protected] wrote:

I feel like the main thing missing from Coq to make passing between bundled and unbundled structures easy is the ability to automatically coerce an unbundled object to a bundled one by invoking a typeclass search. That is, we can declare a coercion pType >-> Type and an IsPointed instance for it, so that elements of pType can be automatically unbundled. But we should also be able to use an element of Type as a pType if an IsPointed instance for it can be found by typeclass search. If we had that, then the bundled and unbundled versions would be silently isomorphic.

It seems to me that something like that could be implemented in a more flexible metalanguage such as Andromeda. But in Coq, we can still do something like the hottclasses:

Class Cast A B := cast: A -> B. Arguments cast _ _ {Cast} _. Notation "' x" := (cast _ _ x) (at level 20) : mc_scope. Typeclasses Transparent Cast.

This doesn't yet do a typeclass search, but what if we had something like

Class Cast {A} B (x : A) := cast : B. Notation "' x" := (@cast _ _ x) (at level 20).

Could we then do something like

Global Instance equiv_cast A B (f : A -> B) `{IsEquiv A B f} : Cast (A <~> B) f := BuildEquiv f _.

and then write ' f to make any function into an equivalence by invoking typeclass search for an IsEquiv instance? If so, this might simplify our lives by eliminating the need for lots of equiv_ lemmas (though I suppose having to go through typeclass search might slow things down).

— 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/1165?email_source=notifications&email_token=AABTNTRDSWG3ZTZQQTGLVRTQ2SHWRA5CNFSM4J7KVTWKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4ICWJ7GA, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTRVBJOWBL4SEE56DPLQ2SHWRANCNFSM4J7KVTWA .

[spitters]

Here is the way type classes are implemented in lean. https://arxiv.org/abs/2001.04301 It's likely that this is useful for Coq too.

One reason why we unbundle classes is to be able to treat diamond inheritance. I estimate that this is less important for equivalences, so Floris' proposal may work well.

On Mon, Feb 3, 2020 at 5:56 PM Floris van Doorn [email protected] wrote:

This comment is also related to #1211 https://github.com/HoTT/HoTT/issues/1211.

My experience with equivalences in Lean is that type-class inference is too slow and (at least in the case of Lean) too brittle. For this reason during development I slowly moved to the direction of using bundled equivalences whenever possible, and almost never use unbundled equivalences (and the same is true for group homomorphisms and any other type class on functions). There are some cases where I still used unbundled equivalences, for example to formulate universal properties. These are usually formulated by stating that some specific (universal) map is an equivalence. When proving universal properties, usually the first lemma I applied was the lemma stating that if e : A <~> B and e == f then isEquiv f (in which case I'm working with bundled equivalences again). When using universal properties, I just used it as a bundled equivalence. This limits the type class problems for equivalences to almost 0. If I would build a library from scratch, I would try not even making isEquiv a class.

There are some patterns of reasoning that are a little trickier with bundled equivalences. For example, if for unbundled equivalences you would apply the lemma isEquiv g -> isEquiv (g o f) -> isEquiv f for bundled equivalences I would have g : B <~> C and gf : A <~>C and then use g ^-1 oE gf and show that this map is homotopic to the function f : A -> B I want to prove to be an equivalence. This is slightly more awkward than the unbundled lemma. However, usually the map from A -> C is not definitionally equal to g o f, but only homotopic to it, and then you need an additional lemma in the unbundled case.

In Coq I've also noticed that type class inference for equivalences is sometimes very slow. One example is demonstrated in #1204 https://github.com/HoTT/HoTT/pull/1204, another one I noticed is the following. Sometimes, when I have f : A <~> B and I write f ^-1, type class inference can still take multiple seconds to find the single instance equiv_isequiv. It is instantaneous when I write f ^-1 % equiv (e.g. here https://github.com/mikeshulman/HoTT/blob/82a893ed7464424fe346dd30f1e832d33f1b7080/theories/Pointed/Core.v#L329 ).

My suggestions:

• Formulate all lemmas about equivalences (also) using bundled equivalences, and make those the "default" ones (e.g. if the lemma using unbundled and bundled equivalences would want the same name, add a prime to the lemma using the unbundled equivalence)
• Encourage bundled equivalences via notation. By default ^-1 and oE should take bundled equivalences as arguments.
• (Slowly) go through the library and use the lemmas formulated with bundled equivalences instead of the ones with unbundled equivalences.

If these suggestions are followed, then bundling up an unbundled equivalence shouldn't need to happen very often, because the equivalences you want to use are already bundled up. I think that if you rely on type-class inference to promote a function to a bundled equivalence, you will regularly run into performance issues.

— 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/1165?email_source=notifications&email_token=AABTNTWAHXPXB2BX4IFWCADRBBEDFA5CNFSM4J7KVTWKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKUSUIY#issuecomment-581511715, or unsubscribe https://github.com/notifications/unsubscribe-auth/AABTNTST6J3TTF5XNLPLQN3RBBEDFANCNFSM4J7KVTWA .

[jdchristensen]

I'm still not convinced about the idea of focusing on bundled equivalences. They are certainly handy a lot of the time. But other times a natural map always exists, but is only an equivalence under some hypotheses. The natural map might pop up in some proof, and then you'd like to have the isequiv lemma at hand to prove it's an equivalence in this case, or even better, have it found by typeclass search. Just a thought...

[mikeshulman]

I don't think anyone is suggesting to do away with isequiv in situations like that. It's only when the map is always an equivalence that there's little point in having an unbundled version.

[jdchristensen]

Sounds reasonable.

[fpvandoorn]

In Lean, what I would do in those cases is to define the function, and define the bundled equivalence separately (depending on the extra assumptions). This is done in such a way that the forward function of the bundled equivalence is definitionally equal to the original function.

As a simple example, you might have

prod_functor (f : A -> A') (g : B -> B') : A * B -> A' * B'
equiv_prod_functor (f : A <~> A') (g : B <~> B') : A * B <~> A' * B'

Instead of using the lemma "prod_functor f g is an equivalence if f and g are" I just used equiv_prod_functor, with which you can prove the same things. This might lead to some reasoning that is different from the reasoning in the HoTT book, but I found it more convenient.

Of course, there is nothing wrong with having both options available.

[mikeshulman]

I think in such cases I would prefer to keep our current approach, with a stated preference for using eq_fmap_prod when we know we have equivalences, but with isequiv_fmap_prod also existing in case it's needed. If nothing else, I think it's good to have the fact that "a specific map is an equivalence" stated explicitly as a theorem, since in many cases that's the correct category-theoretic definition of some universal property (for instance) -- even if in most applications it suffices to use the bundled equivalence knowing that its forward map is defiintionally the specified function.