Преобразование кода Haskell в код Agda

Мы должны преобразовать этот тип данных haskell в код Agda:

data TRUE
data FALSE
data BoolProp :: * -> * where
PTrue :: BoolProp TRUE
PFalse :: BoolProp FALSE
PAnd :: BoolProp a -> BoolProp b -> BoolProp (a `AND` b)
POr :: BoolProp a -> BoolProp b -> BoolProp (a `OR` b)
PNot :: BoolProp a -> BoolProp (NOT a)

Вот что у меня есть до сих пор:

module BoolProp where

open import Data.Bool
open import Relation.Binary.PropositionalEquality

data BoolProp : Set wheree
ptrue : BoolProp true
pfalse : BoolProp false
pand : (X Y : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y)
por : (X Y : Bool) -> BoolProp X -> BoolProp Y -> BoolProp (X ? Y)
pnot : (X : Bool) -> BoolProp X -> BoolProp (not X)

Но я получаю эту ошибку : «Set должен быть типом функции, но не при проверке того, что true является допустимыми аргументами для функции типа Set». Я думаю, что Set нужно изменить на что-то другое, но я не понимаю, что это должно быть.