var a : Type; b < a

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

=

\ ((var f : a ->? b))((var x : a)) .

(var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

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

=

\ ((var f : a ->? b), (var x : a)) .

(var f : a ->? b) ((var f : a ->? b) (var x : a))

as (a ->? b) * a ->? b

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

=

\ ((var f : a ->? a))((var x : a)) .

(var f : a ->? a) ((var f : a ->? a) (var x : a))

as (a ->? b) -> a ->? b

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

. (op twice[a; b] :

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

(var f : a ->? b)

(var x : a)

= (var f : a ->? b) ((var f : a ->? b) (var x : a))

%% Type Variables --------------------------------------------------------

a : Type %(var_1)%

b < a : Type %(var_2)%

%% Assumptions -----------------------------------------------------------

twice

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

%(op)% =

\ ((var f : a ->? a))((var x : a)) .

(var f : a ->? a) ((var f : a ->? a) (var x : a))

as (a ->? b) -> a ->? b

twice2

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

%(op)% =

\ ((var f : a ->? b))((var x : a)) .

(var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

twice3

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

%(op)% =

\ ((var f : a ->? b), (var x : a)) .

(var f : a ->? b) ((var f : a ->? b) (var x : a))

as (a ->? b) * a ->? b

%% Variables -------------------------------------------------------------

f : a ->? b

x : a

%% Sentences -------------------------------------------------------------

forall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

%(def_twice2)%

twice3 = (\ (f : a ->? b, x : a) . f (f x) as (a ->? b) * a ->? b)

%(def_twice3)%

twice = (\ (f)(x : a) . f (f x) as (a ->? b) -> a ->? b)

%(def_twice)%

twice f x = f (f x)

%% Diagnostics -----------------------------------------------------------

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

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

### Hint 9.20, not a class 'a'