Anodyne maps

[fredrik-bakke]

Defines anodyne maps and weakly anodyne maps and establishes some basic closure properties.

[VojtechStep]

How are the changes to descent related to anodyne maps? I can't see from just reading the changes on GitHub where you need those.

[fredrik-bakke]

I've continued work in this branch after the initial work on anodyne maps concluded, since subsequent work depends on this and it tends to take a long while for my work to be reviewed. I'm hoping to formalize Mather's second cube theorem. By the way, how do you feel about renaming "descent data of pushouts" to "reduced descent data of pushouts"? So we can name the thing with an additional family PS over S and two families of equivalences PS ≃ PA ∘ f and PS ≃ PB ∘ g as "descent data of pushouts"?

[fredrik-bakke]

If someone is willing to review my work on anodyne maps then I'm happy to move the changes to descent data of pushouts to a different branch

[fredrik-bakke]

The changes to fiber' are also not needed for anodyne maps. In all, the original part of this PR is about 500 lines.

[fredrik-bakke]

I've preemptively moved the new changes to a different branch

[VojtechStep]

By the way, how do you feel about renaming "descent data of pushouts" to "reduced descent data of pushouts"?

I don't see a reason to. The current development uses this definition, and the cube theorems talk about cartesian transformations.

[fredrik-bakke]

By the way, how do you feel about renaming "descent data of pushouts" to "reduced descent data of pushouts"?

I don't see a reason to. The current development uses this definition, and the cube theorems talk about cartesian transformations.

The proposed definition seems more useful to me, and mirrors the signature of the underlying diagram. For instance, I'm currently working on formalizing the flattening lemma for (expanded) descent data of pushouts, since that's the formulation I need for Mather's cube theorem.

[VojtechStep]

An alternative is to call the type with two equivalences "equifibered spans", precisely because they mirror the shape of a span. For sequential colimits the two notions agree, and the SvDR paper uses "equifibered sequences", so equifibered-sequential-diagram is already in the library, in addition to descent-data-sequential-colimit (which is defined as an alias in this case).

[fredrik-bakke]

Ah, yep, that works, thanks!

[fredrik-bakke]

@VojtechStep Hi again. I read a little up on the origin of the terminology, and being "equifibered" is a property of a natural transformation/display/dependent structure, not the structure itself. I.e., a span can't be "equifibered", but a dependent or displayed span can be, i.e., a span can only be equifibered relative to some other span. In particular, every span is equifibered over itself. This seems to be inconsistent with how you've implemented the terminology in the library. What's the justification for the current terminology usage?

[fredrik-bakke]

If you want a noun for such a structure, one might speak of an equifibration over a span, or equifibration of spans.

[VojtechStep]

I was suggesting that if you have a span σ : A <-f- S -g-> B, then you can call the type (PA : A -> UU) * (PS : S -> UU) * (PB : B -> UU) * (fam-equiv PS (PA . f)) * (fam-equiv PS (PB . g)) the type of equifibered spans over σ. That should be consistent with the standard nomenclature, because if you take the total span, then the first projection will be equifibered (i.e. what being equifibered would mean for a displayed structure).

See that equifibered-sequential-diagram is essentially a dependent sequential diagram bundled with a predicate saying that the maps are fiberwise equivalences. I was thinking about calling it equifibered-sequential-diagram-over or equifibered-sequential-diagram-over-sequential-diagram, but I decided there's no reason to be this explicit in the name, precisely because as you say, equifibrancy is a property of a displayed structure.

[fredrik-bakke]

What you have formalized is an "equifibered dependent sequential diagram", which is different from an equifibered sequential diagram over a sequential diagram, i.e., a morphism of sequential diagram f : A -> B whose fibers are sequential diagrams of equivalences. Can I suggest renaming the formalized concept to equifibered-dependent-sequential-diagram?

[fredrik-bakke]

Sorry, let me elaborate a little. I think the disambiguation/elaboration matters, as the term "equifibered" is not that common, at least, I had not heard of it before, and it sounds similar to other unrelated concepts like "equivariance" and "isofibration". By omitting key terms like "dependent" or "displayed", or "over", the meaning and usage of the term was not clear to me, and I suspect it might not be to others either.

[VojtechStep]

There's precedent for calling dependent structures "fibered"/"over" and their instantiation at a point a "fiber at a"/"over a" , and not reserving those just for the unstraightened versions; both in the library (e.g. fiberwise equivalences) and in type-theoretical literature (e.g. what I formalized is called "a sequence equifibered over (A, a)" in the SvDR20 paper).

Unless you envision formalizing fibers of general morphisms of sequential diagrams and spans, I would strongly prefer to keep the current naming scheme. And even if you do, I'm inclined to believe that they would be less useful/convenient to work with, since by talking about fibers you raise the dimension of identifications you need to care about — I experimented recently with sections of unstraightened fibered sequential diagrams, and it was very painful.

[VojtechStep]

LGTM