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)

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 : b) : 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);

types

Inj : Type -> Type -> Type;

i : Type -> Type -> Type

types

Inj < __->__;

i < __->__

vars

a < b : Type %(var_58)%;

b < c : Type %(var_108)%;

c < e : Type %(var_139)%;

d < f : Type %(var_140)%;

e : Type %(var_137)%;

f : Type %(var_138)%

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

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

%(op)%

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

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 < 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; x : a . up x = (x : b)

forall a < b : Type; e : Type; f : Type; f : e -> f

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

forall

a < b : Type; c < e : Type; d < f : Type; e : Type; f : Type;

f : e ->? d

. (up f : c ->? f) = \ x : a : 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)

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

### Hint 1.15, 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 6.7, not a kind 'a ->? b'

### Hint 6.19, not a class 'a'

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

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

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

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

### Hint 10.17, rebound variable 'f'

### Hint 10.37, not a class 'a'

### Hint 10.40, not a class 'a'

### Hint 10.36, rebound variable 'x'

### Hint 10.6, redeclared type 'Inj'

### Hint 10.22, repeated supertype '__->__'

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

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

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

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

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

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

### Hint 14.13, not a class 'a'

### Hint 14.12, rebound variable 'x'

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

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

### Hint 23.6, not a class 'a'

### Hint 23.5, rebound variable 'x'

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

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

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

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

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

### Hint 28.8, rebound variable 'f'

### Hint 28.39, rebound variable 'x'

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

### Hint 29.8, rebound variable 'f'

### Hint 29.40, rebound variable 'x'

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

### Hint 30.8, rebound variable 'x'

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

### Hint 30.14, rebound variable 'y'