Definition of inner anodyne map

[kyoDralliam]

Adds

• the definition of inner anodyne maps (RS17, def 5.19),
• a proof that Λ²₁ → Δ² is inner anodyne,
• the proof that the pushout product of an inner anodyne cofibration with a cofibration is an inner cofibration (RS17, prop 5.20, also implemented the version with swapped arguments for the cofibrations)
• the proof that Λ³₂ → Δ³ is an inner cofibration (spelled out part of RS17, prop 5.21)

Before merging this PR, various definitions should be renamedt. In particular the names small and large corresponding to the types of extensions against respectively Λ³₂ → Δ³ and Δ³×Λ²₁ ∪_{Λ³₂×Λ²₁} Λ³₂×Δ² → Δ³×Δ² (the pushout product of Λ³₂ → Δ³ and Λ²₁ → Δ²). The names X and h^ could also be changed (but correspond to the names in the paper proof).

Wrt #8, the proof of Λ³₁ → Δ³` being inner anodyne and that of prop 5.21 are missing (Is there a proof of lemma 5.16 already there or should it be added too ? Depends on #7).

[TashiWalde]

I would have expected a stronger definition of is-inner-anodyne, where one asks to uniquely lift against any inner fibration C -> A and not just absolute Segal types C (corresponding to C --> 1).

If we don't take this as the definition, then we should be able to prove it as a characterization.

[emilyriehl]

Hey @kyoDralliam your latest version had a search and replace error (where a type variable X used earlier in the file was replaced with a new term name). I've just pushed a new commit to your branch which fixes that.

[emilyriehl]

I like the changes you've made to the shapes file except I think we should get rid of Λ everywhere and replace it with your new 2,1-horn. Would you like me to make this change or would you prefer to do it?

[kyoDralliam]

Sorry about that, I missed that. Thank you for catching it.

Le mer. 27 sept. 2023, 16:35, Emily Riehl @.***> a écrit :

Hey @kyoDralliam https://github.com/kyoDralliam your latest version had a search and replace error (where a type variable X used earlier in the file was replaced with a new term name). I've just pushed a new commit to your branch which fixes that.

— Reply to this email directly, view it on GitHub https://github.com/rzk-lang/sHoTT/pull/57#issuecomment-1737527901, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAATQU5ZMAZXNB3L2J5AX3LX4Q2RZANCNFSM6AAAAAA5HUG3E4 . You are receiving this because you were mentioned.Message ID: @.***>

[emilyriehl]

The only other thing still to be done is to rename retract , section , and homotopy-retraction-section-id into something more specific to this setting. Any unique name is fine but we should save those generic term names for other use. I think your h^ is fine.

[kyoDralliam]

We can't do that yet because it creates type errors: I define the horn as a subtope of the 2 dimensional simplex while the pre-existing definition is a tope on 2 x 2 and I think rzk does not accept to subtype the latter into the former because 2 x 2 is a cube and not a tope.

Le mer. 27 sept. 2023, 16:36, Emily Riehl @.***> a écrit :

I like the changes you've made to the shapes file except I think we should get rid of Λ everywhere and replace it with your new 2,1-horn. Would you like me to make this change or would you prefer to do it?

— Reply to this email directly, view it on GitHub https://github.com/rzk-lang/sHoTT/pull/57#issuecomment-1737530537, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAATQU3S4JTVJ6NIET5LKQDX4Q2W7ANCNFSM6AAAAAA5HUG3E4 . You are receiving this because you were mentioned.Message ID: @.***>

[emilyriehl]

We can't do that yet because it creates type errors: I define the horn as a subtope of the 2 dimensional simplex while the pre-existing definition is a tope on 2 x 2 and I think rzk does not accept to subtype the latter into the former because 2 x 2 is a cube and not a tope. Le mer. 27 sept. 2023, 16:36, Emily Riehl @.***> a écrit :

I see your point. I'll mention this to @fizruk .