strengthen definition of inner anodyne

[TashiWalde]

In #57, inner anodyne maps are defined via unique lifting against Segal types C.

• Define the notion of inner fibrations C -> A (including the possibility that A and C are not Segal).

• Prove the stronger unique lifting property of inner anodyne maps against all inner fibrations.

If this turns out not to be possible, we should strenghten the definition of inner anodyne.

[TashiWalde]

Now that a robust calculus of right orthogonal maps and unique extension types is mostly in place, it is time to address this question not just in the special case of Λ ⊂ Δ², but for general shape inclusions.

@kyoDralliam are you still interested in working this out? If not, I would like to take this on.

[kyoDralliam]

I won't have the time to tackle this soon, so please go ahead @TashiWalde

[TashiWalde]

After thinking about this for a bit, I have some comments:

1) It is definitely not the case that for two arbitrary shape inclusions j : ϕ ⊂ ψ and j' : ϕ' ⊂ ψ', the following are equivalent:

• j' is genuinely j-anodyne, i.e. every map right orthogonal to j is also right orthogonal to j'.
• j' is weakly j-anodyne (what is currently called "anodyne"), i.e. every type with unique j-extensions has unique j'-extensions. For example, the two shape inclusions {0} ⊂ Δ¹ and {1} ⊂ Δ¹ are weakly anodyne for each other (because the class of types with unique extensions are in both cases the groupoids), but they are not genuinely anodyne for each other (because covariant fibrations are not the same as contravariant fibrations).

2) This means that if the statement is true for the inner horn inclusion (i.e. for inner anodyne), it must be due to some non-trivial thing about that specific shape inclusion, not just some formal argument. I wonder if @emilyriehl had something in mind here when writing RS17?

[TashiWalde]

In light of the changes made in #126, I'll close this issue.