# Zulip Chat Archive

## Stream: new members

### Topic: type constraints

#### Henning Dieterichs (Nov 02 2020 at 12:40):

I have a type `T`

and a fixed predicate `P: T -> Prop`

. Can I make a type X, so that `x: X`

implies `x: T and P(x)`

?

I guess composition can be used to achieve that, but I would need to use `x.t`

to get the underlying `T`

:

```
def T: Type := ℕ → ℕ
def P : T → Prop
| f := (∀ n: ℕ, (f n < n))
structure X := mk :: (t : T) (prop : P(t))
def foo : ∀ x: X, x.t 10 < 10 := sorry
```

Are there ways so that X is automatically casted to T?

I don't feel type classes help much, compared to just requiring P as hyptothesis.

```
class X (t: T) := (prop: P t)
def foo { x: T } [X t] : x 10 < 10 := sorry
```

Can I somehow state `{ x: X }`

and obtain `{ x: T } [X t]`

?

#### Johan Commelin (Nov 02 2020 at 12:42):

I think you are looking for subtypes: `{x : T // P x}`

#### Adam Topaz (Nov 02 2020 at 12:43):

Checkout `subtype P`

#### Johan Commelin (Nov 02 2020 at 12:43):

Or, without notation `subtype P`

.

#### Johan Commelin (Nov 02 2020 at 12:45):

Henning Dieterichs said:

I have a type

`T`

and a fixed predicate`P: T -> Prop`

. Can I make a type X, so that`x: X`

implies`x: T and P(x)`

?

You cannot have `x : X`

implies `x : _`

. A term has 1 type (up to definitional equality). Also, you cannot *prove* that `x`

has type `X`

or type `T`

. It can only be *checked* by the type checker.

#### Henning Dieterichs (Nov 02 2020 at 12:55):

Thanks, subtype is exactly what I was looking for!

Last updated: May 18 2021 at 16:25 UTC