# Atomic judgments¶

Red**PRL** currently has five forms of atomic (non-hypothetical) judgments that may appear in subgoals.

- Truth asserts that a type is inhabited.
- Type equality asserts an equality between two types.
- Subtyping asserts a subtyping relation.
- Subkinding asserts that some type is actually a universe in which all types has a particular kind.
- Term lets the user give an expression.

Note that these judgment forms differ from our semantic presentations in papers.

## Truth¶

A *truth* judgment

```
a true
```

or simply

```
a
```

means `a`

is an inhabited type.
Any inhabitant can realize this judgment.
For example, the expression `1`

realizes

```
int
```

because `1`

is in the type `int`

.
This is commonly used
to state a theorem or specify the type of the program to be implemented.
In fact, all top-level theorems (see Defining theorems) must be in this judgmental form.

## Type equality¶

A *type equality* judgment

```
a = b type
```

means `a`

are `b`

are equal types (without regard to universe level),
and its realizer must be `ax`

, the same as the realizer of equality types.
For example, we have

```
int = int type
```

realized by `ax`

.
Multiverses are supported through kind markers such as `kan`

or `discrete`

:

```
a = b discrete type
a = b kan type
a = b coe type
a = b hcom type
a = b pre type
```

where `a = b kan type`

means `a`

and `b`

are equal Kan types.
(The judgment `a = b type`

is really an abbreviation of `a = b pre type`

because `pre`

is the default kind.)
Following the PRL family of proof assistants
which use partial equivalence relations,
well-typedness is defined as the equality of the type and itself;
to save some typing, `a type`

stands for `a = a type`

and `a kan type`

stands for `a = a kan type`

.

In the presence of universes and equality types, one might wonder why we still have a dedicated judgmental form for type equality. That is, one may intuitively treat the judgment

```
a = b type
```

as `(= (U l) a b) true`

for some unknown universe level `l`

.
It turns out to be very convenient to state type equality without specifying the universe levels;
with this, we survived without a universe level synthesizer as the one in Nuprl,
which was created to alleviate the burden of guessing universe levels.

## Subtyping¶

A *subtype* judgment

```
a <= b type
```

states that `a`

is a subtype of `b`

. More precisely, the partial equivalence relation
associated with `a`

is a subrelation of the one associated with `b`

.
The realizer must be `ax`

.
There is no support of kind markers because the subtyping relation
never takes additional structures into consideration.

This is currently used whenever we only need a subtyping relationship
rather than type equality. For example, if a function `f`

is in type `(-> a b)`

,
the rule to determine whether the function application `($ f x)`

is in type `b'`

will only demand `b <= b' type`

rather than `b = b' type`

.
That said, the only non-trivial subtyping relation one can prove in Red**PRL** now
is the cumulativity of universes. One instance would be

```
(U 0 discrete) <= (U 1 kan)
```

realized by `ax`

.

## Subkinding¶

The following are *subkind* judgments:

```
a <= discrete universe
a <= kan universe
a <= coe universe
a <= hcom universe
a <= pre universe
```

They assert that `a`

is a subuniverse of the universe of the specified kind at the omega level.
Intuitively, `a <= k universe`

would be the subtyping judgment `a <= (U omega k) type`

if we could internalize universes at the omega level.
The realizer must be `ax`

.
These judgments play the same role as subtyping judgments
except that they handle the cases where the right hand side is some omega-level universe.
Suppose a function `f`

is in type `(-> a b)`

.
The rule to determine whether the function application `($ f x)`

is a type
will demand `b <= pre universe`

rather than `b = (U omega) type`

(or `b = (U l) type`

for some universe level `l`

).

## Term¶

A *term* judgment is displayed in the sort of the expression
it is asking for, for example:

```
dim
exp
```

The realizer is the received term from the user.
This is used to obtain motives or dimension expressions.
For example, the `rewrite`

tactic requires users to specify
the parts to be rewritten by fulfilling *term* subgoals.