# NOTE: dependent type language

This is a brief note about what a type theory should have and the flow.

## 1. Top level

A top level of dependent type language should be a modular thing,
whatever a module or big `letrec`

. In the top level, we should be able
to have a list of definitions, these definitions should be able to
reference each others. We will need an independent context for these,
and use elaboration to break them down into core AST.

### 1.1. Elaboration

This step converts top level definition like ```
data=(inductive family),
=let
```

, or `letrec`

into a set of bindings from identifier to the core
term. For example

- inductive data type
`let`

is definition that will not recursively refer to self and with syntax like`let var : type = term`

, hence, we could apply function`check`

from check component`check term type`

ensure the term has type- extends the global context
`var`

to`type`

in type context(or record type information in value, I'm not sure it's always work)`var`

to`term`

in value context

`letrec`

will refer to self, this is important feature when implementing function- introduce de Bruijn indices as local context?

## 2. Check component

This component should verify

`checkType term`

: given term is a valid type`check term type`

: given term has type- infer type of
`term`

produces`tm_type`

- invokes
`equateType type tm_type`

- infer type of

## 3. Inference component

Produces a type from a term

## 4. Equate component

This component should verify

`equateType context type tm_type`

: normalized types are same under the context`equate context value value`

: values are same under the context

## 5. Evaluate component

This component should produce value from term, for example, converts below

M : \Pi (x : A). B[x] --------------------- M(C) : B[x\C]