1N/Atype p a := Pred (Pred a)

1N/A %% should be correct

1N/Atype

1N/Atype m b := b

1N/A %%

1N/Atype m b := b

1N/A %% both contradict

1N/Atypes

1N/Am : -Type -> Type;

1N/Ap : +Type -> Type

1N/Atypes

1N/Am := \ b : -Type . b;

1N/Ap := \ a : +Type . Pred (Pred a)

1N/A### Hint 2.27-2.32, wrong covariance of 'a'

1N/A### Hint 2.27-2.32, no kind found for 'a'

1N/A*** Error 2.27-2.32, no kind found for 'Pred a'

1N/A*** Error 4.6,

1N/Aincompatible kind of: m

1N/A expected: -Type -> Type

1N/A found: +Type -> Type

1N/A