AgdaのHaskell型式のメーターが `Raw`で始まっているのはなぜですか？

Question

Agda標準ライブラリでは、我々はRawMonad、RawApplicative、などがあります。..

RawMonad : ∀ {f} → (Set f → Set f) → Set _ 
RawMonad M = RawIMonad {I = ⊤} (λ _ _ → M) 

RawMonadZero : ∀ {f} → (Set f → Set f) → Set _ 
RawMonadZero M = RawIMonadZero {I = ⊤} (λ _ _ → M) 

RawMonadPlus : ∀ {f} → (Set f → Set f) → Set _ 
RawMonadPlus M = RawIMonadPlus {I = ⊤} (λ _ _ → M) 

は、なぜ彼らはRawで始まるのですか？ AgdaにMonadまたはApplicativeはありますか？

Answer 1

私はNils Anders Danielsson（彼らの著者、私は疑いがあります）は、それぞれの法律の証拠が含まれていないという理由でそれを聞いたことがあります。 AFAIK、Agda標準ライブラリには、そのような証明を含むこれらのバージョンはありませんが、必要に応じて独自のロールを使用することができます。