Basics of (oo,n)-categories

[mikeshulman]

Here's my next iteration of coinductive wild oo-categories.

Change # 1: By getting rid of (oo,oo)-categories and considering only (oo,n)-categories for finite n, the proof that equivalences compose becomes much simpler, and little if any interesting generality is lost -- the only true (oo,oo)-categories that I know of are things like the (oo,oo)-category of (oo,oo)-categories, and at the moment I don't think that even has a "wild" version since the amount of coherence required to even define a k-transfor seems to go up with k.

Change # 2: I simplified the notion of HasEquivs to include only the property CatIsEquiv, with a bundled version CatEquiv defined uniformly for all categories. I think this is easier to read and work with; the only drawback is that at present, @CatEquiv Type doesn't coincide with Equiv. However, I think that can be finessed, either by bringing the basic category definitions into Basics, or by using a general notion of subtype for both of them. For examples other than Type, such as pType, there's no problem since they are defined later in the library and can simply use CatEquiv explicitly instead of whatever manual definition they already had.

Change # 3: There is now a "default" coherent definition of HasEquivs using bi-invertibility that can be used for any category if desired, thus simplifying the process of defining a category. But I kept the option for users of defining a different one, so that if it's desired to use half-adjoint equivalences (e.g. for Type) that can be done. (I tried making the default definition use half-adjoint equivalences, but that was much harder than bi-invertibility since you need associativity and unit isomorphisms to even state the adjoint coherence law.)

Change # 4: I defined dependent inserters directly rather than in terms of comma categories. I think this way is clearer, partly because it doesn't require product categories. We can then define comma categories in terms of them (but I didn't yet).

Change # 5: I added some results about truncated categories, including a general notion of "isomorphism" for (1,1)-categories that could be plugged into (for instance) groups, etc. rather than separately defining GroupIsomorphism and so on in each case separately.

Overall I'm trying to figure out whether this development can be made "lightweight" and comprehensible enough to be "the" categories library we use everywhere, replacing the current truncated-only definitions in WildCat. An aspect of that would be to make it possible for users to use only finitely many dimensions, rather than being forced to work with infinitely many in all cases. It's already possibly to talk about categories with only finitely many dimensions of cells, just by sticking in Unit at the top of the coinductive notion. But there isn't yet a way to talk about functors that only act on finitely many dimensions if their domain and codomain categories were defined to include infinitely many. I think it should be possible to do this by parametrizing functors by a "coherence dimension", but I haven't tried yet.

I'm interested in any feedback, but particularly about the feasibility of this idea. Could this actually be usable by anyone? Or is it unavoidably just too scary-looking and heavyweight?

I do think this approach would have some practical advantages. For instance, having the higher morphisms and equivalences around from the beginning deals more cleanly with a definition of 2-category than our previous version that required explicitly passing to cores on hom-categories. And it allows us to formulate general notions of universal property (e.g. reflective subcategories) that specialize in particular cases to our funext-free versions (e.g. reflective subuniverses).

[Alizter]

make spits out loads of warning because Fibrations is now an ambiguous name.

[mikeshulman]

Bah

[mikeshulman]

I've been thinking for a while that it might be better to rename HoTT.Fibrations to HoTT.HFiber.

[JasonGross]

make spits out loads of warning because Fibrations is now an ambiguous name.

This is why I always fully qualify everything. Note that I have a tool that should be able to do this automatically, if so desired.

[Alizter]

cate_compose_temp has a universe error on one of the jobs. I suspect this is a coq bug.

[Alizter]

coherence required to even define a k-transfor seems to go up with k.

Exactly which coherence is this? Might it be possible to coinductively add the necessary coherence?

Change # 4: I defined dependent inserters directly rather than in terms of comma categories. I think this way is clearer, partly because it doesn't require product categories. We can then define comma categories in terms of them (but I didn't yet).

Is there any point defining one in terms of the other? Why not just define them separately?

It's already possibly to talk about categories with only finitely many dimensions of cells, just by sticking in Unit at the top of the coinductive notion. But there isn't yet a way to talk about functors that only act on finitely many dimensions if their domain and codomain categories were defined to include infinitely many.

Well I don't think that is the correct way to do finite dimensional cells. We are in HoTT, which means every type comes equipped with a full oo-groupoid structure. I would rather that "finite dimensional" categories begin using regular paths as higher cells. Then we can always characterize the action of functions on paths anyway using ap.

So if I were to define a 2-cat X as some oo-cat, I would define the two dimensions and then say the higher cells are just paths. When I construct functors X -> Y, then I need only supply the action on the first two dimensions since the action on paths is always given.

In general I think this is cool. It is a bit scary as you say though. It took me some time to get on board with the (oo,n) idea, but I see why it make some more practical sense than (oo,oo).

One of the things I noticed with the (oo,oo)-definition is that it is relatively easy to show pType is a globular type. I struggled a lot trying to show it was a Cat0.

Will it ever be possible to define some sort of functor category? If not, it looks less likely that we can characterise (co)limits.

[mikeshulman]

I would rather that "finite dimensional" categories begin using regular paths as higher cells.

Yes, that's another option which is certainly better than just using Unit, but it's more work -- not at the level of IsGlob, but at the level of IsCat0 and beyond where you'll start having to explain how the operations you defined at lower dimensions act on those paths. So I would say that's sort of a middle road between the total cop-out of Unit and the morally right path of giving a correct funext-and-univalence-free definition of all the higher cells.

I have no doubt that with the right approach we'll be able to characterize (co)limits. That might or might not involve defining a functor category.

[mikeshulman]

I tried pType; it does seem that the brute force approach isn't going to work. I'm sure there's a way to do it in this case, but this makes me think that maybe we'd need another level of parametrization: someone might want to be able to define an IsGlob instance that goes up at all dimensions, but an IsCat0 instance on the same type that only goes up some finite number of dimensions. Is it going to get unmanageable to have an extra "dimension level" of parametrization on every typeclass?

[mikeshulman]

I think I see how to get pType as a displayed 0-coherent category over Type, although I haven't managed to push it all the way through yet: there's a missing precomposition lemma, and a universe issue when trying to sigma it up, plus the 0-coherence lemma for sigmas of displayed categories isn't complete.

[mikeshulman]

And, of course, dimension restrictions on the coherence of functors will infect categories as well, since we use functors to construct categories (inserters, comma categories, etc.).

It would be pleasing if we could simply parametrize categories by an (n,r) as in (n,r)-category, where n can be infinity but r cannot. Then n would be a limit on the dimensions of stuff, r a bound on invertibility, and of course there will still be a coherence index as always that would be the only difference with "classical" higher category theory. Functors and transfors would have only an n bound, I guess.

There will probably be some mins involved when performing constructions. Unless we behave like Coq's universe polymorphism and assume m <= n and m <= p instead of using min(n,p). Along those lines, I have been wondering whether it would be reasonable to make inequality of natural numbers and trunc indices into typeclasses in general.

[Alizter]

I have been wondering whether it would be reasonable to make inequality of natural numbers and trunc indices into typeclasses in general.

Trunc index inequality is currently a type class.

[mikeshulman]

Oh my, you're right. Is it used anywhere?

[Alizter]

@mikeshulman I think I made it a typeclass when I was doing the Trunc_min stuff. That should be in Truncations/Core.v

[Alizter]

So for 2-categories there is a notion of "hom-wise core". Do we have something similar but for only 1-cells? I imagine such an example wouldn't fit into the (oo,n)-framwork.

Actually I'm not even sure this is possible. Can you have invertible lower cells without invertible higher ones?

[mikeshulman]

Yes, of course you can. The end result won't be describable as an (n,r)-category, but it makes sense to discard the noninvertible 1-cells and keep all the 2-cells between the invertible ones.

[Alizter]

@mikeshulman Do you know of any examples of this being done in 2-cat literature?

[mikeshulman]

Not offhand.

[Alizter]

Hmm, an example where this might be done would be to take a monoidal category C. Then consider it's 2-category delooping BC. For whatever reason, you might be interested in the sub 2-category that consists of "objects with inverses". Then this "lower core" would correspond to some sort of categorification of taking the subtgroup of invertible elements in a monoid.

I also suspect there would be a Grothendieck-like construction that would correspond to formally inverting all the lower cells, though I am not sure what the higher cells for those would be.

[Alizter]

@mikeshulman Could you rebase this?

[JasonGross]

Nit:

Suggested change

	(** The natural numbers are defined in [Coq.Init.Datatypes] (we weren't able to excise them from the stdlib), and studied further in [Spaces.Nat]. But her we give some basic definitions. *)
	(** The natural numbers are defined in [Coq.Init.Datatypes] (we weren't able to excise them from the stdlib), and studied further in [Spaces.Nat]. But here we give some basic definitions. *)

Also, I think this is no longer true as of #1429

[JasonGross]

I think it might make more sense have these be aliases for IsTrue (n =? 0) and IsTrue (n >? 0)? (I think one lesson from ssreflect is that reasoning is easier if you keep all decidable predicates in bool and only move to Prop at the very end.)

[JasonGross]

Again, maybe we want to go through a boolean equality on trunc_index?

[JasonGross]

Do we want also an only printing notation for @Hom (pred 0) _ _ a b?

[JasonGross]

nit: You use notation for IsGlob, why not also for IsDGlob?

Suggested change

	@IsDGlob (pred m) (a $-> b) (pred n) (fun f => DHom a b f u v) _ ;
	@IsDGlob m.-1 (a $-> b) n.-1 (fun f => DHom a b f u v) _ ;

[JasonGross]

You could use something like u $-{ f }-> v?

[mikeshulman]

I think I tried that, but found it unreadable in practice.

[JasonGross]

I've rebased this at https://github.com/JasonGross/HoTT/tree/pr/1302, fixed the build conflicts, and also fixed the universe issue (and reported it as coq/coq#14057).

[JasonGross]

Would it be useful to have a telescoped version of this, where B is of type forall (a : A) (b : B a) (c : C a b) ..., Type? I think I could probably code up a version where n was a tuple of nats whose size is given by the length of the telescope (though perhaps it makes more sense to index the telescope over its length, so we can talk about two telescopes of the same length), and I could probably code up enough typeclass / canonical structure magic that you would just do something like IsDGlob (n1, n2, n3) (fun x y z => W) and it would be able to infer the necessary types automatically.

[Alizter]

@JasonGross I would be interested in this telescoping idea, could you write a small example?

[JasonGross]

I don't have it fully figured out, but here's what I have so far:

Set Universe Polymorphism.
Set Implicit Arguments.
Set Primitive Projections.
Record sig A P := exist { pr1 : A ; pr2 : P pr1 }.
Arguments sig (A P)%type.
Notation "{ x | P }" := (sig (fun x => P)) : type_scope.
Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope.
Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope.
Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope.
Notation "n '.-1'" := (pred n) (at level 9, format "n '.-1'") : nat_scope.
Notation "n '.+1'" := (S n) (at level 9, format "n '.+1'") : nat_scope.
Notation "( x ; y )" := (exist _ x y) : fibration_scope.
Notation "( x ; .. ; y ; z )" := (exist _ x .. (exist _ y z) ..) : core_scope.
Fixpoint telescope (n : nat) : Type :=
  match n with
  | 0 => unit
  | n.+1 => { A : Type | A -> telescope n }
  end.
Fixpoint Sigma {n} : telescope n -> Type
  := match n with
     | 0 => fun _ => unit
     | n.+1 => fun '(A; B) => { a : A | Sigma (B a) }
     end.
Fixpoint Pi {n} : forall t : telescope n, (Sigma t -> Type) -> Type
  := match n with
     | 0 => fun _ B => B tt
     | n.+1 => fun '(A; t) B => forall a : A, Pi _ (fun s => B (a; s))
     end.

I haven't yet figured out what the right types are, but I think we need to bundle IsDGlob to get this to work. The next step is to write something that takes in n : nat and spits out { A : Type | { B : A -> Type | { C : forall a, B a -> Type | ... } } }. I think I did this once before, and it's a bit tricky but doable. This is the type that we parametrize the generalization of IsGlob/IsDGlob over. Then we write a thing that takes in one of these sigmas and spits out the type of all the hom fields, again as a sigma. Then, finally, we take in an element of this sigma and perform the appropriate transformation to turn it back into a thing we can pass to IsGlob. In this case, passing n := 0 will turn this coinductive into IsGlob judgmentally. Passing n:=1 should turn it into, roughly { IsGlob A | IsDGlob B }.

[JasonGross]

I think something like this should work, but it's giving me universe inconsistencies:

Fixpoint Homs {n} : forall (tA tB : telescope n), Type
  := match n with
     | 0 => fun 'tt 'tt => unit
     | n.+1 => fun '(A; P) '(B; Q) => forall (a : A) (b : B), { Hom : Type | @Homs n (P a) (Q b) }
     end.
Fixpoint Homs_cps {n} : forall {tA tB}, (telescope n -> Type) -> @Homs n tA tB -> Type
  := match n with
     | 0 => fun 'tt 'tt F 'tt => F tt
     | n.+1
       => fun '(A; P) '(B; Q) cont Hom
          => forall (a : A) (b : B),
              @Homs_cps n (P a) (Q b) (fun t => cont (pr1 (Hom a b); (fun _ (* ??? *) => t))) (pr2 (Hom a b))
     end.
Inductive Homs_cps_ind : forall {n tA tB}, (telescope n -> Type) -> @Homs n tA tB -> Type :=
| Homs0 : forall F, F tt -> @Homs_cps_ind 0 tt tt F tt
| HomsS : forall {n} A P B Q cont Hom,
    (forall (a : A) (b : B), @Homs_cps_ind n (P a) (Q b) (fun t => cont (pr1 (Hom a b); (fun _ (* ??? *) => t))) (pr2 (Hom a b)))
    -> @Homs_cps_ind (n.+1) (A; P) (B; Q) cont Hom
.
CoInductive IsGlob@{u} (n : nat) (A : Type@{u}) : Type :=
  {
    Hom : A -> A -> Type@{u} ;
    isglob_hom : forall (x y : A), IsGlob n.-1 (Hom x y) ;
  }.
CoInductive IsDGlob@{u} (n : nat) {A : Type@{u}} (B : A -> Type@{u}) : Type :=
  {
    DHom0 : A -> A -> Type@{u}
    ; DHom1 : forall (a b : A) (f : DHom0 a b) (u : B a) (v : B b), Type@{u}
    ; isdglob_dhom : forall (a b : A) (u : B a) (v : B b),
        @IsDGlob (pred n) (DHom0 a b) (fun f => @DHom1 a b f u v) ;
  }.
CoInductive IsGenGlob (n : nat) {len} (t : telescope len) : Type :=
  {
    GHom : Homs t t
    ; isgenglob_ghom : Homs_cps_ind (IsGenGlob n) GHom
  }.

There's a ??? where I'm not sure that I set things up right. I expect that you should be able to prove IsGlob here equivalent to IsGenGlob (len:=0) and IsDGlob here (which is bundled) equivalent to IsGenGlob (len:=1). It also shouldn't be hard to generalize to a tuple of nats rather than a single one, since the nats are independent from the types.

[JasonGross]

I don't suppose Coq will accept

Suggested change

	Arguments fmapD {_ _ _ _ _ _} F {_ a b} f.
	Arguments fmapD {_ _ _ _ _ _} F {_ a b} f, {_ _ _ _ _ _} F {_} a b f.

? (I think it won't because fmapD is a DHom which might unfold to be a type of unknown arity.) If it did, you wouldn't need fmapD' below.

[Alizter]

I did not know you could give multiple declarations of arguments! The documentation still seems a bit sparse but this is cool feature.

[JasonGross]

Does typeclass resolution backtrack across successes of multisuccess tactics? If so, you might be able to do something like

Suggested change

	Ltac change_dim n :=
	match n with
	| (pred ?m) => fail 1
	| _ => progress change n with (pred (S n))
	end.
	Ltac change_dim_0 n :=
	match n with
	| (pred ?m) => fail 1
	| 0%nat => progress change 0%nat with (pred 0)
	end.
	Ltac change_dim n :=
	multimatch n with
	| (pred ?m) => fail 1
	| _ => progress change n with (pred (S n))
	| 0%nat => progress change 0%nat with (pred 0)
	end.

[JasonGross]

Is it important that IsDGlob is indexed over the globular structure of A, rather than providing the globular structure of both A and B at once? The reason I ask is because there seems to be a nice generalization to telescopes that makes IsGlob the base case and IsDGlob a sort of inductive step, but I think it requires bundling all the globular structure as fields rather than parameterizing over it, I think.

[JasonGross]

I'm struggling to understand how this fits into the picture. Can you elaborate on it a bit more?

The perspective I'm coming from is that it seems like all of the dependent globular theory should generalize to telescopes (i.e., from forall a, B to forall a b ... c, D), and I'm trying to understand what the telescope picture looks like here. Does doing this in a telescope way require defining globular maps mutually with globular types?

[JasonGross]

I think this should be parameterized over laxity, so that we get things to line up more judgmentally. What do you think?

[JasonGross]

Should we also add

Definition lcat_compose {l : Laxity} `{IsCat1 n A} {a b c : A} (f : lHom l a b) (g : lHom l b c) : lHom l a c

?

[JasonGross]

Is there a reason for using this structure rather than talking about adjoint equivalences? They're the same, right, just involving a reshuffling of data?

[JasonGross]

I'm a bit confused by the n=0 comment, since it seems that gpd_inv is not enough to fill qiso_issect and qiso_isretr? I think this means we should be indexing "(oo,n)-category" starting with n = -1, not n = 0, so that the inverses we get are actually connected to the identity? Or is there a deep/good reason that we're not considering categories to be truncated at levels above n?

[JasonGross]

Thinking a bit more about this, it seems like maybe gpt_inv should be removed entirely, and its content is subsumed by being truncated one level up?

[JasonGross]

Which bug is this? (Maybe add a reference in the comment?)

[Alizter]

coq/coq#12975 which will be fixed by coq/coq#9711

[JasonGross]

Is this supposed to be empty?

[JasonGross]

Technically, wouldn't the latter involve moving cat_id, isfunctor0_postcomp and isfunctor0_precomp to IsCat1, because cat_id takes a 0-cell to a 1-cell, and the pre/post comp functor instances take 1-cells to 2-cells?

[JasonGross]

Can you elaborate on this a bit more? If we were to fully go with the "at most 1 dimension of difference between input and output", would that mean getting rid of isfunctor1_{pre,post}comp?

[JasonGross]

One way to let the user specify this is to make a typeclass for "is already adjointified" and another one for "might already be adjointified" (where we add a high-cost instance for "it's not" to "might already be adjointified", and a lower cost instance from "it is adjointified" to "it might be"). Then these lemmas could take in the optional class, and adjointify only if we don't have a proof in hand that it's already adjointified, and then we could prove the coherence regardless of what instance is passed in, and we could prove that passing in a "already adjointified" instance preserves all the homotopies.

[JasonGross]

Why is this commented?

[JasonGross]

What's up with the set?

[JasonGross]

There's a more general version of this, where you can go from pseudo to any laxity, right?

[JasonGross]

Maybe we should have flip : Laxity -> Laxity or something and this should be more general?

[JasonGross]

What's the relationship between comma categories and inserters?