Anodyne shape inclusions

[TashiWalde]

I have formulated the general concept of anodyne shape inclusions relative to any fixed shape inclusions.

Currently there is a little terminology clash here that we need to resolve:

• I have defined S->T to be anodyne for U->V if every map right orthogonal to U->V is also right orthogonal to S->T.
• There is also a variant, where instead of right orthogonal maps one only considers right orthogonal types. This gives a strictly weaker notion of anodyne which I have temporarily called "weak anodyne".
• In RS17, and as currently implemented in 05-segal-types, "inner anodyne" is defined to be (equivalent to) "weak anodyne for Λ ⊂ Δ²", rather than "anodyne".

My vote goes to keeping "anodyne" and "weak anodyne" as described above and changing the RS17 definition to "weak inner anodyne". I think this is more in line with standard terminology.

Moreover, it seems like one should be able to strengthen the current proof in 05-segal-types and show that the inner 3-horn is not just weak anodyne but actually anodyne for the inner 2-horn.

See also the comments I made in #64 .

[emilyriehl]

@TashiWalde I agree with your preferred terminology. Would you mind making that change and noting that "weak-anodyne" corresponds to "anodyne" in the paper? Then this looks good to go.