Subshapes

[emilyriehl]

In the sHott library we have two closely related definitions:

#def Λ : (2 × 2) → TOPE
  := \ (t , s) → (s ≡ 0₂ ∨ t ≡ 1₂)

#def Λ²₁ : Δ² → TOPE
  := \ (t,s) → Λ (t,s)

I attempted to delete the former and use only a direct definition of the latter but a few things in the Segal file then failed to typecheck. The issue was in the definition of is-segal-function-type which feeds the horn into the function flip-ext-fun-inv.