vars a : -Type; b : +Type

types i a b, Inj a b < a -> b

vars a : Type; b < a

op twice : (a ->? b) -> (a ->? b)

type F a b

%% should be illegal here

vars f : a ->? b; x : a

. twice f x = f (f x);

vars a : Type; b : Type

type Inj a b = {f : a -> b . forall x, y : a . f x = f y => x = y}

vars a, b : Type; a < b

op down : b ->? a

vars y : b; x : a

. down y = x;

op up : a -> b

. down (up x : b) = x

. def (down y : a) => up (down y : a) = y;

vars c : Type; b < c

var x : a

. up (up x : b) = (up x : c)

. up (x : a) = (x : b);

vars c, d, e, f : Type; c < e; d < f

forall f : e -> f . (up f : e ->? f) = \ x : e . f x;

forall f : e ->? d . (up f : c ->? f) = \ x : c . up (f (up x));

forall x : c; y : d

. (up (x, y) : e * f) = (up x, up y)

. forall f : e -> d . (up f : c -> f) = \ x : c .! f (up x);

types

F : Type -> Type -> Type;

Inj : -Type -> +Type -> Type;

i : -Type -> +Type -> Type

types

Inj < __->__;

i < __->__

vars

a < b : Type %(var_24)%;

b < c : Type %(var_42)%;

c < e : Type %(var_57)%;

d < f : Type %(var_58)%;

e : Type %(var_55)%;

f : Type %(var_56)%

op down : forall b : Type; a < b : Type . b ->? a

op twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

op up : forall b : Type; a < b : Type . a -> b

vars

f : a ->? b;

x : a;

y : b

forall a : Type; b < a : Type; f : a ->? b; x : a

. twice f x = f (f x)

forall a : Type; b : Type

. forall f : a -> b

. (f in Inj a b) <=> forall x, y : a . f x = f y => x = y

forall a < b : Type; b : Type; x : a; y : b . down y = x

forall a < b : Type; b : Type; x : a . down (up x : b) = x

forall a < b : Type; b : Type; y : b

. def (down y : a) => up (down y : a) = y

forall a < b : Type; b < c : Type; c : Type; x : a

. up (up x : b) = (up x : c)

forall a < b : Type; b < c : Type; c : Type; x : a . up x = (x : b)

forall e : Type; f : Type; f : e -> f

. (up f : e ->? f) = \ x : e . f x

forall c < e : Type; d < f : Type; e : Type; f : Type; f : e ->? d

. (up f : c ->? f) = \ x : c . up (f (up x))

forall c < e : Type; d < f : Type; e : Type; f : Type; x : c; y : d

. (up (x, y) : e * f) = (up x, up y)

forall c < e : Type; d < f : Type; e : Type; f : Type

. forall f : e -> d . (up f : c -> f) = \ x : c .! f (up x)

### Hint 1.6, is type variable 'a'

### Hint 1.16, is type variable 'b'

### Hint 2.8, rebound type variable 'a'

### Hint 2.10, rebound type variable 'b'

### Hint 3.6, is type variable 'a'

### Hint 3.6, rebound type variable 'a'

### Hint 3.15, rebound type variable 'b'

### Hint 7.7, not a kind 'a ->? b'

### Hint 7.19, not a class 'a'

### Hint 10.6, is type variable 'a'

### Hint 10.6, rebound type variable 'a'

### Hint 10.15, is type variable 'b'

### Hint 10.15, rebound type variable 'b'

### Hint 11.17, rebound variable 'f'

### Hint 11.37, not a class 'a'

### Hint 11.40, not a class 'a'

### Hint 11.36, rebound variable 'x'

### Hint 11.6-11.8, redeclared type 'Inj'

### Hint 11.22-11.23, repeated supertype '__->__'

### Hint 13.6, is type variable 'a'

### Hint 13.6, rebound type variable 'a'

### Hint 13.9, is type variable 'b'

### Hint 13.9, rebound type variable 'b'

### Hint 13.18, rebound type variable 'a'

### Hint 15.7, not a class 'b'

### Hint 15.13, not a class 'a'

### Hint 15.12, rebound variable 'x'

### Hint 22.6, is type variable 'c'

### Hint 22.15, rebound type variable 'b'

### Hint 24.6, not a class 'a'

### Hint 24.5, rebound variable 'x'

### Hint 28.6, is type variable 'c'

### Hint 28.6, rebound type variable 'c'

### Hint 28.9, is type variable 'd'

### Hint 28.12, is type variable 'e'

### Hint 28.15, is type variable 'f'

### Warning 28.15,

type variable does not shadow normal variable 'f'

### Hint 28.24, rebound type variable 'c'

### Hint 28.31, rebound type variable 'd'

### Hint 29.9, not a class 'e'

### Hint 29.9, not a class 'f'

### Hint 29.8, rebound variable 'f'

### Warning 29.8, variable also known as type variable 'f'

### Hint 29.39, rebound variable 'x'

### Hint 30.9, not a kind 'e ->? d'

### Hint 30.8, rebound variable 'f'

### Warning 30.8, variable also known as type variable 'f'

### Hint 30.40, rebound variable 'x'

### Hint 31.9, not a class 'c'

### Hint 31.8, rebound variable 'x'

### Hint 31.15, not a class 'd'

### Hint 31.14, rebound variable 'y'

### Hint 31.33,

no kind found for 'e'

expected: {Cpo}

found: {Type}

### Hint 31.33,

no kind found for 'e'

expected: {Cppo}

found: {Type}

### Hint 33.11, not a class 'e'

### Hint 33.11, not a class 'd'

### Hint 33.10, rebound variable 'f'

### Warning 33.10, variable also known as type variable 'f'

### Hint 33.40, rebound variable 'x'