isofibration API

Stream: Infinity-Cosmos

[Emily Riehl]

I've been working on expanding the blueprint for the infinity-cosmos project to introduce more low-hanging fruit: namely the definitions, constructions, and lemmas now appearing in section 1.4 (warning: the lemmas vary considerably in difficulty). To make this feasible I've been working on developing some basic API around the isofibrations in an infinity-cosmos.

[Emily Riehl]

But I have no idea how to develop good API for further formalization! So I'd love it if folks had a look at this file to offer comments and suggestions (and it would be great if someone filled in the final pesky sorry).

[Emily Riehl]

On paper, the oo-cosmos axioms are used to construct various new objects (new oo-categories in the oo-cosmos) and new maps between them (new oo-functors). These are all just objects and morphisms in the underlying 1-category of the oo-cosmos, though the axioms assume that various limits exist and are simplicially enriched. But enriched conical limits are in particular ordinary unenriched limits and Lean knows this now in all the cases we need (I believe).

[Emily Riehl]

Specific questions:

• should these terms have different names?
• is it bad to have so many non-computable definitions?
• should I have the simptags at the lemmas I've simped?
• should anything be an instance?
• what is missing?

If anyone wants to contribute further extensions please go ahead!

[Johan Commelin]

is it bad to have so many non-computable definitions?

I wouldn't worry about that. It just means that we can't let the kernel compute with these definitions. But we weren't really planning on doing that anyways.

You could start your file with noncomputable section (and finish the file with end) so that you can remove the noncomputable keyword everywhere.

[Johan Commelin]

should I have the simptags at the lemmas I've simped?

Those look good to me. The final lemma in the file also looks like a good simp lemma.

[Johan Commelin]

should anything be an instance?

The rule of thumb is: if X is a class, and your definition is providing the canonical term of type X, then you can make your definition into an instance.

[Johan Commelin]

should these terms have different names?

As far as I can see, the names look good.

[Nick Ward]

Maybe there is a reason for avoiding this (e.g. naming), but I think many of the lemmas like compIsofibration_map can be automatically generated by tagging the corresponding def with @[simps]. In the case of compIsofibration_map, the generated lemma is called compIsofibration_coe.

[Nick Ward]

Tagging the def with @[simps?] will print the generated simp lemmas for comparison.