bicategory

Stream: new members

[Yuma Mizuno]

In these days I write a formalization of bicategories. I have finished writing a proof that the collection of pseudofunctors between bicategories have a bicategory structure, so I would like to PR it to mathlib.

When writing basic lemmas on bicategories, almost all lines are copied from category_theory/monoidal/category.lean. I added 0-morphisms and replaced tensors with left and right whiskerings.

Currently, I use the following notations

infixr `◃`: 70: = bicategory.whisker_left
infixr `▹`: 70: = bicategory.whisker_right
notation `α_`: = bicategory.associator
notation `λ_`: = bicategory.left_unitor
notation `ρ_`: = bicategory.right_unitor

that are used in the nlab (https://ncatlab.org/nlab/show/bicategory), but I'm not sure if this is good or not.

[Yaël Dillies]

cc @Bhavik Mehta, who also formalized bicategories

[Junyan Xu]

Hi @Yuma Mizuno, I just noticed your bicategory-functor branch by accident and want you know about my ongoing work at lax_grothendieck, where I defined lax functors from a 1-category to the 2-category of categories Cat, and use it to make the Grothendieck construction of fibration of categories. I see a few issues that would prevent my branch from using your development, and I hope you have these in mind during your development:

(1) you only defined pseudofunctors and not general lax functors, i.e. you require map_id and map_comp to be isos, but I think the more general lax functors are preferable, and shouldn't take much more effort; my earlier idea is to make the structure pseudofunctor by extending lax_functor by the is_iso conditions, but now I think we don't need to define pseudofunctor separately, and can just rely on the type class mechanism to infer the is_iso instances for map_id and map_comp. In fact in my construction of colimits in Grothendicek categories, only map_comp is required to be iso.

(2) The direction of your map_id and map_comp are in the opposite direction to mine. Your direction agrees with nLab, but mine is the natural direction to make the Grothendieck construction in the current form. (I am refactoring the existing Grothendieck construction that only applied to strict functors, and the old setup forces me to adopt this direction.)

Thanks for your work and your consideration!

[Yuma Mizuno]

Thank you for the comments and letting me know about your ongoing work @Junyan Xu ! I was a little hesitant to use is_iso because it doesn't have the inverse as data, but I'll try to use it. My choice of the directions of map_id and map_comp was completely random, and I have no idea which direction should be chosen for pseudofunctors. (A similar choice appears in the definition of pseudonatural transformations.)

[Yuma Mizuno]

I think the Yoneda lemma for bicategories needs pseudofunctor as a structure.

[Adam Topaz]

I think it might be worthwhile to define pseudofunctors with isos instead of is_iso for exactly the reason that sometimes it may be useful to have the inverse as data. Besides, if we have lax pseudofunctors, we would presumably also want oplax pseudofunctors, so choosing one direction doesn't make much sense.

[Junyan Xu]

I don't think we need oplax functors for the same reason we don't need contravariant functors; it makes no sense to duplicate the functor API. Oplax can be obtained from lax by taking opposites of the same categories (the fiber categories in the Grothendieck construction case).

[Junyan Xu]

Yuma Mizuno said:

I think the Yoneda lemma for bicategories needs pseudofunctor as a structure.

If that's the case then indeed that would be a reason to introduce the structure. Literature suggests that we also need pseudofunctor to show the projection functor from the Grothendieck construction is a Grothendieck fibration of categories, which I plan to do after the colimit work.

[Junyan Xu]

And by the way, I did come up with an example of lax natural transformation in my colimit work: https://github.com/leanprover-community/mathlib/compare/lax_grothendieck?expand=1#diff-779e8ece193ac9cfb8b3ab087590457d8f57c59a774bd663d70eaa8e6a160ecdR242

[Junyan Xu]

My direction of arrows is natural in the sense that if we have colimits in the base and fiber categories, then we get colimits in the total (Grothendieck) category, and it also agrees with the old Grothendieck construction. @Yuma Mizuno 's direction would lead straightforwardly to PresheafedSpace and alike, but there we need colimits in the base category and limits in the fiber categories to get colimits in the total category (e.g. PresheafedSpace).

[Junyan Xu]

Also, the inv in an iso here isn't actually data, as it's uniquely determined by the hom. In general I think it's OK to replace sugsingletons with Props, except maybe for the purpose of defeq. e.g. is_limit could be made a Prop (in fact docs#Top.presheaf.is_sheaf is defined as nonempty is_limit), but is_left_adjoint is actually data. When I get to work on Grothendieck fibrations, I'd probably make is_fibration carry the data of a cleavage.

[Adam Topaz]

There are times where it's very useful to be able to actually use the definition of an inverse. There is a reason why we have both docs#category_theory.iso and docs#category_theory.is_iso, docs#category_theory.equivalence and docs#category_theory.is_equivalence (edit: this is not a great example, since the inverse is part of this structure), and even why has_inv is required for a group structure.

[Kevin Buzzard]

We have equiv and function.bijective

[Junyan Xu]

category.equivalence is not a good example also because the inverse is only unique up to isomorphism. Maybe you can come up with examples where the inverse of map_id or map_comp are useful? In all examples I have in mind they're either eq_to_hom or eq_to_hom transferred across adjunction in an abstract way, and only one direction is needed to define the category structure on the Grothendieck construction. If you want to use the definition of the inverse, you could show exists.some is equal to the definition and rewrite, barring defeq issues.

[Yuma Mizuno]

I updated bicategory-functor and changed iso to hom in the definition. I think it is not a bad idea to start with hom instead of iso as a first step, whether or not we really need pseudofunctors. I also reversed the directions of hom s in the definition, in the hope that it will fit well @Junyan Xu 's ongoing work.

[Yuma Mizuno]

By the way, 2-categories have two types of opposites. I don't have a good idea for implementation of these concepts. My naive idea is to duplicate the contents in data/oppoiste.

[Junyan Xu]

Currently if a type C carries a category instance, then C^op carries the opposite category instance. I think in order to make four types to carry the four possible opposite bicategory instances, we would need to introduce another ^op operation that yields a new type given an old type, possibly called ^hop for "hom op" (I think that name isn't taken yet), which only reverses arrows in the hom categories. But we would face the problem that (C^op)^hop is not the same as (C^hop)^op, which is similar to the problem that +1 and -1 don't commute definitionally when people attempted to define chain complexes. But I think it's not too bad as we can show they are equivalent, like the equivalence between C and (C^op)^op already in mathlib.

[Andrew Yang]

I think would occasionally be hard to rewrite because of dependent type issues.
Would it be possible for a pseudofunctor to accept a field of a nat_iso and a proof that the two are equal?
The same thing could probably also be tried on the monoidal category library.

[Junyan Xu]

To Yuma Mizuno: I see you encountered issues with "obviously" from your commit messages. I think they can sometimes be useful, but sometimes they produce timeouts. When it timeouts, you can just supply the field with a faster explicit proof to avoid the timeout. Sometimes when you just finish the definition of earlier fields but has not supplied some "obvious" fields, the orange bar may take a long time to disappear, which indicates that Lean is trying to fill in the "obvious" fields, and once you add , some_field_name := , indicating you're gonna supply some_field_name explicitly, the orange bar may disappear much faster. So in general I think removing "obviously" doesn't buy you anything and you should try to keep them, if there're no issues that I'm unaware of.

[Junyan Xu]

Andrew Yang said:

I think would occasionally be hard to rewrite because of dependent type issues.

At least when the target of the pseudo/oplax functor is Cat, map_id and map_comp are nat_iso / nat_trans and rewriting won't break the .app ... It may be best to wait until when we actually use the inverses (like the Yoneda lemma) to decide which approach to adopt.

[Yuma Mizuno]

@Junyan Xu said

So in general I think removing "obviously" doesn't buy you anything and you should try to keep them, unless there're issues that I'm unaware of.

The timeout I encountered occurred when defining oplax functors by the structure command. In a new commit I succeeded in preserving obviously by adding an auxiliary definition for a long equation in the axiom of oplax functors. This seems to work well because restate axiom automatically expands the auxiliary definitions and generates a desired lemma.

[Junyan Xu]

I've written down a definition of bicategories in terms of the composition functor; this shortens the definition by encapsulating many axioms into properties of functors and natural transformations. However, the pentagon and triangle axioms are quite lengthy when expressed as equality of natural transformations, and it may be easier to write them down as equality between the .app after ≫, ◁, ▷ are defined in terms of the composition functor. For simplicity I replaced isos with homs.

import category_theory.products.associator
namespace category_theory
universes w v u
class bicategory (B : Type u) extends quiver.{v+1} B :=
(hom_category : ∀ (a b : B), category.{w} (a ⟶ b) . tactic.apply_instance)
(comp (a b c : B) : (a ⟶ b) × (b ⟶ c) ⥤ (a ⟶ c))
-- encompass `whisker_left_(id,comp), whisker_right_(id,comp), whisker_exchange (category.theory.bifunctor.diagonal)`
(associator (a b c d : B) : (comp a b c).prod (𝟭 _) ⋙ comp a c d ⟶
   prod.associator _ _ _ ⋙ (𝟭 _).prod (comp b c d) ⋙ comp a b d)
-- encompass naturality
(id (a : B) : a ⟶ a)
(left_unitor (a b : B) : prod.sectr (id a) _ ⋙ comp a a b ⟶ 𝟭 _)
(right_unitor (a b : B) : prod.sectl _ (id b) ⋙ comp a b b ⟶ 𝟭 _)
-- encompass naturality
(pentagon (a b c d e : B) : let
  l1 := whisker_right (nat_trans.prod (associator a b c d) (𝟙 (𝟭 _))) (comp a d e),
  l2 := whisker_left ((prod.associator _ _ _ ⋙ (𝟭 _).prod (comp b c d)).prod (𝟭 _)) (associator a b d e),
  l3 := whisker_left ((prod.associator _ _ _).prod (𝟭 _) ⋙ prod.associator _ _ _)
    (whisker_right (nat_trans.prod (𝟙 (𝟭 _)) (associator b c d e)) (comp a b e)),
  r1 := whisker_left (((comp a b c).prod (𝟭 _)).prod (𝟭 _)) (associator a c d e),
  r2 := whisker_left (prod.associator _ _ _ ⋙ (𝟭 _).prod (comp c d e)) (associator a b c e)
  in l1 ≫ l2 ≫ l3 = r1 ≫ r2)
(triangle (a b c : B) : let
  l1 := whisker_left ((prod.sectl _ (id b)).prod (𝟭 _)) (associator a b b c),
  l2 := whisker_right (nat_trans.prod (𝟙 (𝟭 _)) (left_unitor b c)) (comp a b c) in
  l1 ≫ l2 = whisker_right (nat_trans.prod (right_unitor a b) (𝟙 (𝟭 _))) (comp a b c))

[Junyan Xu]

I don't know if this is a simplification for what you want to do with them, though. I'll look into applying this approach to lax functors tomorrow. Note: the let expressions above are necessary, since if you substitute them in, you'd encounter unification errors and would have to insert ≫ eq_to_hom (by exact rfl).

[Yuma Mizuno]

Junyan Xu said:

For simplicity I replaced isos with homs. (Are such bicategories ever studied in the literature?)

I found they are called skew bicategories in https://arxiv.org/abs/1408.4953.

[Junyan Xu]

I've been able to define oplax functors in terms of map functors, map_id morphisms, and map_comp natural transformations, posted as a gist.
However, it seems Lean core typechecking is very slow on the map_unitor's, and I get deterministic timeouts unless one of the map_unitor's is commented out. The problem is probably that curry_obj is not defined in terms of sectr, so a lot unfolding is necessary for Lean to see that things are defeq. In contrast, map_associator is parsed/checked very quickly, though I didn't add any obviously. An interesting observation is that unlike the .app/componentwise version in #11277, in the nat_trans version I must insert t between r1 and r23, because the two functors aren't defeq (but are in fact equal): on object level they're actually defeq, so { app := λ _, 𝟙 _ } is a nat_trans between them, and that's why you don't need to insert t in the componentwise version; on the map level, their equality depends on functor.map_id of the functor map a a (or map b b). In contrast, functor.map_comp isn't required to state the three equalities.

[Johan Commelin]

Can you insert an identity somewhere to prevent the unfolding? If you have

my_target_is_X ≫ my_source_is_X_but_this_needs_heavy_unfolding

Then you can write

def Im_just_id : X ⟶ complicated_version_of_X := 𝟙 _

my_target_is_X ≫ Im_just_id ≫ my_source_is_X_but_this_needs_heavy_unfolding

Now, if you use Im_just_id multiple times, you've won something. Because you've replaced many heavy rfls by 1 single heavy rfl.

[Junyan Xu]

There's one heavy rfl in the r23 in the definition of map_left_unitor and a heavy rfl in the r23in the definition of map_right_unitor, and in each case it appears just once. Of course once the structure oplax_functor is defined, these rfls will be used implicitly whenever you construct a oplax_functor.

[Junyan Xu]

I think introducing

@[simps] def sectr_functor : C ⥤ D ⥤ C × D :=
{ obj := λ Z, sectr Z D,
  map := λ X Y f, { app := λ Z, (f, 𝟙 Z) } }

in category_theory/products/basic and using it instead of curry_obj would help, and moreover curry_obj can be defined in terms of it, but refactoring it will be a bigger project as currying.lean is imported by four files...

[Junyan Xu]

today I learned 𝟭 C ⋙ F is defeq to F ⋙ 𝟭 D, but neither is defeq to F (as I knew before, and associativity of functor composition is also defeq)...

[Kevin Buzzard]

I thought that equality of functors was evil?

[Junyan Xu]

In the map_left_unitor equality, the type of the target of the left hand side is 𝟭 (a ⟶ b) ⋙ map a b, while for the right hand side it is map a b ⋙ 𝟭 (obj a ⟶ obj b), so it works "by accident". I could append unitors (and also insert associators) as is done in triangle identities in adjunction, but that feels unnecessary and cumbersome to me, and in my tests it doesn't speed things up. Using sectr_functor or using bicategory.id directly instead of the notation 𝟙 of the category_structure instance constructed from bicategory also does little to speed.

The strange thing I observed is that things get slower inside structure. After I introduce auxiliary definitions, the structure itself speeds up to ~28s (no longer timeouts). Stuff outside of structure are fast:

parsing took 3.16ms
elaboration of map_associator_aux took 439ms
type checking of map_associator_aux took 352ms
decl post-processing of map_associator_aux took 0.12ms
compilation of category_theory.map_associator_aux took 2.06ms

parsing took 1.92ms
elaboration of map_left_unitor_aux took 3.63s
type checking of map_left_unitor_aux took 133ms
decl post-processing of map_left_unitor_aux took 0.142ms
compilation of category_theory.map_left_unitor_aux took 2.65ms

parsing took 1.86ms
elaboration of map_right_unitor_aux took 3.54s
type checking of map_right_unitor_aux took 164ms
decl post-processing of map_right_unitor_aux took 0.13ms
elaboration: tactic compilation took 0.474ms

But if I inline map_associator, the structure slows down from ~28s to ~47s. With both map_associator and map_left_unitor inlined, it slows down to ~86s, but if you do by { clear map_associator, exact ... } when defining map_left_unitor, then it speeds up to ~49s; so it seems earlier fields will interfere and slow down later fields even when the later field doesn't depend on the earlier field.

[Junyan Xu]

I'm trying to adapt my lax_grothendieck branch to the new bicategory API, but I immediately run into a problem:

import category_theory.bicategory.locally_discrete
universes w v u
open category_theory
variables {C : Type u} [bicategory.{w v} C] (X Y : C) (f : X ⟶ Y)
#check f ⟶ f  -- : Type v

while if we import basic instead of locally_discrete, then f ⟶ f will be of Type w, which is what we want. The problem is that once locally_discrete is imported, then this instance takes precedence, even though X Y : C not X Y : locally_discrete C. How should we avoid this? Make locally_discrete irreducible?

Making the instance take a [category C] instead of [category_struct C] would solve this particular example, but if C is a strict bicategory, then we get a [category C] instance and so C would still be endowed with the locally_discrete bicategory structure instead of the original one. I wonder why discrete_category doesn't suffer from this problem. This works as intended:

import category_theory.discrete_category
universes v u
open category_theory
variables {C : Type u} [category.{v} C] (X : C) (Y : discrete C)
#check X ⟶ X -- Type v
#check Y ⟶ Y -- Type u

[Reid Barton]

Making locally_discrete irreducible should work (or more precisely, doing whatever we do for opposite). I'm not sure why this is necessary, though--I thought that ordinary defs should not get unfolded during instance search, but with traces enabled it's clear that locally_discrete is getting unfolded.

[Reid Barton]

I think the discrete analogue works "by chance" based on the order of trying instances--except it's not really by chance because we need to go through category C, and I believe the local instance will always be tried first. Whereas in the locally_discrete case there are two paths and the local instance is not used directly at the branch point.

[Junyan Xu]

The other solutions I can think of are:

1. make locally_discrete a structure with one field, which would require certain mk to construct its terms, but using irreducible also requires first defining helper functions like op and unop before making it irreducible.
2. tweak the priority of the instance involved, which may be a simpler solution.

[Reid Barton]

I guess "other" means other than fixing(?) Lean to not expand this definition during instance search

[Junyan Xu]

Well in solution 1 the new structure isn't the same type as the original one, certainly not defeq, so Lean certainly can't reduce it to the original type during instance inference ...

[Junyan Xu]

irreducible is also effectively making a new type and I'd have to use analogues of op, unop and quiver.hom.op to transfer between objects and morphisms in these two categories on two different types, and this would be the price I have to pay to use the bicategory API to talk about a oplax functor from a 1-category (with locally discrete bicategory structure) to Cat, while I don't have to do this if I take the direct approach in my branch.

[Adam Topaz]

Personally I like the structure approach. For one, you can use angle brackets as the anonymous constructor, whereas with an irreducible def you have to always remember what you named the constructor

[Junyan Xu]

I also used set_option trace.class_instances true to take a look.
The correct instance is
@category_struct.to_quiver (X ⟶ Y) (@category.to_category_struct (X ⟶ Y) (@bicategory.hom_category C _inst_1 X Y)),
which is one step shorter than the wrong instance
@category_struct.to_quiver (X ⟶ Y) (@category.to_category_struct (X ⟶ Y) (@locally_discrete.quiver.hom.category_theory.small_category C (@bicategory.to_category_struct C _inst_1) X Y)), which is puzzling.
Changing attribute [instance] bicategory.hom_category to [instance, priority 1001] fixes the problem. If no one objects I'm gonna adopt this approach.

[Junyan Xu]

With the priority tweak, I have been able to define oplax functors from a 1-category I to a strict bicategory with a simpler definition similar to that in the lax_grothendieck branch, and connect them to general oplax functors from locally_discrete Ito the same strict bicategory via an equiv. I think this is a important special case worthy of a separate simpler definition.

This work revealed certain problems in @Yuma Mizuno's oplax_functor definition (I regret that I didn't catch them during review), namely that map₂_associator', map₂_left_unitor' and map₂_right_unitor' are opposite to the simplification direction, so the auto-generated simp lemmas also point to the "wrong" direction. This can be seen from the need of .symm in lines 106-110. (For the associator, the direction of simplication should be from (f ≫ g) h to f (g ≫ h), in analogy to f ≫ (g ≫ h) = f ≫ g ≫ h.)

[Yuma Mizuno]

For the chaining inferences problem, moving category_theory.discrete_category (X ⟶ Y) into the definition of locally_discrete_bicategory is a possible solution. Although in this approach one cannot give an instance of small_category, but instead just category, this does not seem to cause the elaborator looking for a small_category to miss X ⟶ Y for X Y : locally_discrete C (probably because small_category is defined as abbreviation, not def?).

[Junyan Xu]

That's a good idea too! And yes abbreviation is definitely more transparent than def.

[Yuma Mizuno]

I just realized that the direction of map₂_associator' etc. are subtle.

The current direction is natural at least for general bicategories in the sense that the axioms say that "an oplax functor preserves the associator, left unitor, and right unitor".

[Junyan Xu]

Yeah I now see the subtlety. If you regard a term not involving map₂ to be simpler than terms that involves it, then the current direction is good. But in my use case the part involving map₂ always simplifies to eq_to_hom ...

[Kevin Buzzard]

I've certainly seen examples where you seem to want certain lemmas to be simp one way when you're building the API but the other way when you're using it

[Yuma Mizuno]

Yuma Mizuno said:

For the chaining inferences problem, moving category_theory.discrete_category (X ⟶ Y) into the definition of locally_discrete_bicategory is a possible solution.

I noticed that the elaborator fails to find quiver (X ⟶ Y) for X Y : locally_discrete B in this solution (I don't understand why). So I think @Junyan Xu 's solution (adjustment of priority) is better. I guess setting locally_discrete.hom_small_category to priority 900 (some number less than 1000) also works.

[Junyan Xu]

@Yuma Mizuno Yes I saw you changed priority in your PR and was wondering why. Can you post a #mwe where the quiver instance doesn't work? The following is working for me in my lax_grothendieck_bicat branch, where your suggestion is adopted:

import category_theory.bicategory.locally_discrete
universes v u
open category_theory
variables {C : Type u} [category.{v} C] (X Y : locally_discrete C)
instance : quiver.{v+1} (X ⟶ Y) := by apply_instance

(but if C is only a category_struct then the category instance on X ⟶ Y no longer exists)

[Yuma Mizuno]

import category_theory.bicategory.locally_discrete
universes v u
open category_theory
variables {C : Type u} [category.{v} C]
instance : Π X Y : locally_discrete C, category.{v} (X ⟶ Y) := by apply_instance
/-
tactic.mk_instance failed to generate instance for
  Π (X Y : locally_discrete C), category (X ⟶ Y)
state:
C : Type u,
_inst_1 : category C
⊢ Π (X Y : locally_discrete C), category (X ⟶ Y)
-/

Now I understand that the difference between quiver and category is not irrelevant, but the position of arguments is relevant.

[Junyan Xu]

Yes whether X Y are under binder matters. λ X Y, by apply_instance works

[Yuma Mizuno]

Yes, but I would like to explain why I needed the version of instance whose arguments are under the binder. I defined prelax_functor from locally_discrete (paths B) here, which requires Π (a b : locally_discrete (paths B)), quiver (a ⟶ b) due to the definition of prelax_functor.

[Junyan Xu]

interestingly, by apply bicategory.hom_category also works

[Junyan Xu]

I wonder why this is failing:

[class_instances] (0) ?x_0 X Y : category (X ⟶ Y) := @bicategory.hom_category (?x_1 X Y) (?x_2 X Y) (?x_3 X Y) (?x_4 X Y)
failed is_def_eq