towards a correct definition of an infinity-cosmos

Stream: Infinity-Cosmos

[Emily Riehl]

Over the summer @Mario Carneiro and I sketched a definition of an infinity cosmos that cut several corners (principally around simplicially enriched limits) and left open a few sorries. Thanks to the collective efforts of this group, they have now almost all been resolved.

The draft PR contains two versions of the definition for comparison and commentary and one sorry, which I'll now describe.

[Emily Riehl]

In the code below exact this fails because two instances do not agree:

variable (K : Type u) [Category.{v} K]
variable [SimplicialCategory K]


/-- A `PreInfinityCosmos` is a simplicially enriched category whose hom-spaces are quasi-categories
and whose morphisms come equipped with a special class of isofibrations.-/
class PreInfinityCosmos extends SimplicialCategory K where
  [has_qcat_homs : ∀ {X Y : K}, SSet.Quasicategory (EnrichedCategory.Hom X Y)]
  IsIsoFibration : MorphismProperty K

namespace InfinityCosmos

variable {K : Type u} [Category.{v} K][SimplicialCategory K] [PreInfinityCosmos.{v} K]

open PreInfinityCosmos

/-- Common notation for the hom-spaces in a pre-∞-cosmos.-/
abbrev Fun (X Y : K) : QCat where
  obj := EnrichedCategory.Hom X Y
  property := by
    have : PreInfinityCosmos K := by infer_instance
    have := this.has_qcat_homs (X := X) (Y := Y)
    -- exact this
    convert this
    sorry

One of them is a metavariable I believe(?); I don't really know what this means.

The other is something called toSimplicialCategory. I have no idea what this is and couldn't find it by searching.

[Emily Riehl]

Instances are the bane of my existence, so help would be very welcome.

[Dagur Asgeirsson]

I didn't have permission to push to your branch, but I closed the sorry in https://github.com/emilyriehl/infinity-cosmos/pull/40

The issue was that you had instance variables [SimplicialCategory K] and [PreInfinityCosmos K]. So Lean was confused by the fact that you had a random simplicial category structure on K, and the simplicial category structure coming from the pre-infinity-cosmos structure. The solution was to just remove the [SimplicialCategory K] variable

[Dagur Asgeirsson]

Feel free to just copy my code over to your branch and close my PR so you can keep working on this

[Dagur Asgeirsson]

I've added the instances that make section tests compile (with a sorry)

[Dagur Asgeirsson]

I figured out how to make a PR to your PR instead: https://github.com/emilyriehl/infinity-cosmos/pull/41

[Emily Riehl]

Dagur Asgeirsson said:

The issue was that you had instance variables [SimplicialCategory K] and [PreInfinityCosmos K]. So Lean was confused by the fact that you had a random simplicial category structure on K, and the simplicial category structure coming from the pre-infinity-cosmos structure. The solution was to just remove the [SimplicialCategory K] variable

I see the issue I didn't understand before. When a class extends another class you should only assume an instance of the largest class.

I had somehow thought that for extensions Lean would unify the instances (because I thought [Category K] [SimplicialCategory K] was an example of this). But SimplicialCategory does not extend Category.

[Emily Riehl]

Can you explain the code

attribute [instance] has_terminal has_products

I don't know quite what this does or when to use it.

[Emily Riehl]

One additional note about this PR:

There is one further modification we will definitely make either pre or post merge, which is to use the general enriched category theory of cotensors developed by @Daniel Carranza in place of the stubby material which is currently in the simplicial category cotensors file.

[Dagur Asgeirsson]

Emily Riehl said:

Can you explain the code

attribute [instance] has_terminal has_products

I don't know quite what this does or when to use it.

What it's doing is making the fields has_terminal and has_products of the class InfintyCosmos' instances (the namespace InfinityCosmos' is open).

So it does the same as the following:

instance {K : Type*} [Category K] [InfinityCosmos' K] : HasConicalTerminal K

instance {K : Type*} [Category K] [InfinityCosmos' K] : HasConicalProducts K

[Johan Commelin]

In particular, this means that typeclass synthesis is now aware of them, and can make use of those results when trying to fill in some [FooBar X Y Z] assumption.

[Emily Riehl]

After today's seminar, we now have a sorry-free definition of an oo-cosmos that is actually correct which can be found here. (Confidential to @Daniel Carranza, I did my best to reproduce your code and finish the proof of local_cotensor_bifunctoriality but likely did thing suboptimally.)

There's a lot that needs golfing before we start to build on top of it. I don't have time to highlight specific inefficiencies/questions now but let me just say that suggestions are very welcome.

[Johan Commelin]

Nice milestone! Congrats!

[Emily Riehl]

I'm ready to merge this branch now, unless anyone objects. I'm sure we'll make further tweaks but I want this development to be part of main.