module ImprHIT.Background.WSuspension where

open import Agda.Primitive renaming (Set to Type)

record WSusSig {ℓ ℓ' ℓ''} : Type (lsuc ((lsuc (ℓ ⊔ ℓ')) ⊔ ℓ'')) where
  constructor wSusSig
  field
    Shape    : Type ℓ
    Position : Shape → Type ℓ'
    paths : Type ℓ''
    leftE, rightE : paths -> Shape