\import Logic

\class BaseSpace (E : \Type)

\class InhSpace \extends BaseSpace
  | isInh : TruncP E