module Definition.Typed.Restrictions
{a} (M : Set a)
where
open import Definition.Untyped M
open import Tools.Function
open import Tools.Level
open import Tools.Unit
record Type-restrictions : Set (lsuc a) where
no-eta-equality
field
Unit-allowed : Set a
ΠΣ-allowed : BinderMode → (p q : M) → Set a
Π-allowed : M → M → Set a
Π-allowed = ΠΣ-allowed BMΠ
Σ-allowed : SigmaMode → M → M → Set a
Σ-allowed = ΠΣ-allowed ∘→ BMΣ
Σₚ-allowed : M → M → Set a
Σₚ-allowed = Σ-allowed Σₚ
Σᵣ-allowed : M → M → Set a
Σᵣ-allowed = Σ-allowed Σᵣ
BindingType-allowed : BindingType → Set a
BindingType-allowed (BM b p q) = ΠΣ-allowed b p q
open Type-restrictions