Functorial isomorphism of shape inclusions

[TashiWalde]

• Prove a "cube"-lemma for homotopy cartesian squares.

• Define in terms of representables what it means for two shape inclusions ϕ ⊂ ψ and ζ ⊂ χ to be isomorphic. In practice such isomorphism can easily be specified by explicit formulas involving the coordinates of the cubes.

• Show that isomorphic shape inclusions are anodyne for each other.

---

Side remark for @fizruk : For these sort of constructions it would be very convenient if rzk would support some rudimentary meta-programming features. For example, it would be nice if I could define a macro (syntax just as an example)

#macro @isomorphism-shape-inclusions (repg ; repf)
  :=
    ( \ A →
      ( repg
      , ( ( repf , \ _ → refl)
        , ( repf , \ _ → refl)))
    , \ A _ →
      ( \ repg
      , ( ( repf , \ _ → refl)
        , ( repf , \ _ → refl))))

and then define

#def isomorphism-0-Δ¹-1-right-leg-of-Λ
  : isomorphism-shape-inclusions
    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
    2 Δ¹ (\ t → t ≡ 0₂)
  := @isomorphism-shape-inclusion
     ( \ τ (t,s) → τ s
     ; \ υ s → υ (1₂ , s))

and have the compiler automatically do a syntactic-expansion of the macro @isomorphism-shape-inclusion before type-checking.

In the specific example above it is not too bad, since the formula defining the map of shapes is so short. But it one defines isomorphisms or maps on more complicated shapes, the formulas may involve case distinctions and become long; in that case repeating them multiple times can quickly make the code explode.

Note that there is no way to make this macro into an actual function (without some polymorphism) because different instances of \ τ (t,s) → τ s have different types.

[emilyriehl]

I had a similar thought in the past about whether it would be possible to automatically format a proof of is-equiv in the special case where your proof is an iso (meaning consists of an inverse pair of functions and two reflexive homotopies).