module subtype {l : Level} (Context : Set l) where

record DataSegment {ll : Level} (A : Set ll) : Set (l @$\sqcup$@ ll) where
  field
    get : Context @$\rightarrow$@ A
    set : Context @$\rightarrow$@ A @$\rightarrow$@ Context