## 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