[Agda] subset types? refinement types? type synonyms? type abbreviations?

[Nils Anders Danielsson]

On 2011-11-10 23:27, Ramana Kumar wrote:
> I know one could define raw terms then take a subset of it
> (although not sure how to concretely do that in Agda), but is it
> possible to define well-typed terms all at once without using an
> indexed type?

I'm not sure exactly what you're asking for. Maybe something like the
following?

   data Type : Set where
     _⟶_ : (σ τ : Type) → Type

   data Term : Set

   type : Term → Type

   data Term where
     _·_ : ∀ {σ} (t₁ t₂ : Term) → type t₁ ≡ (type t₂ ⟶ σ) → Term

   type (_·_ {σ = σ} _ _ _) = σ

I don't recommend using this definition.

>>> Formula : Bool ->    Set
>>> Formula = Term bool

> But that code fails in Agda. I tried to define it like that and it
> wouldn't load.

Try making the indices explicit:

   data Term : Type → Bool → Set where
     …

-- 
/NAD