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

[Ramana Kumar]

Suppose I have defined an inductive datatype in Agda representing
Higher-Order Logic terms, indexed by their type.
So I have
  data HOLTerm : HOLType -> Set where ...

Now suppose I want to create a type HOLFormula that picks out the
terms whose type is boolean.
(Suppose I have booltype : HOLType in Agda.)
What are my options? How can I do that?

I am pretty new to Agda, so it might be a simple question with a simple answer.

Will I be able to use HOLFormulas pretty much the same way as HOLTerms
(pattern matching on them the same etc.) except I know that their type
is bool (and am obliged to prove it when I provide one to a function)?

If that's possible, is there a chance of using similar techniques to
define HOLTerm in a non-indexed way, but so that it still captures all
and only the well-typed HOL terms? The reason why I am using an
indexed type at the moment is that some of the constructors require
terms coming in with a certain type. For example

App : forall {x} {y} -> HOLTerm (fun_type x y) -> HOLTerm x -> HOLTerm y

But if I could define subtypes of HOLTerms mutually with the
definition of HOLTerms, there would be a chance of avoiding the
indexing...