b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedervar a : Type; b < a

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederop twice2 :

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

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

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

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder =

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

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

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

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder =

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

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

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedervar f : a ->? b; x : a

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder. (op twice[a; b] :

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (var f : a ->? b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (var x : a)

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

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maeder%% Type Variables --------------------------------------------------------

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedera : Type %(var_1)%

2986838ec286d67e7c199e7ea81e7364ca36ad25Christian Maederb < a : Type %(var_2)%

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Assumptions -----------------------------------------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder(var f : a ->? a) ((var f : a ->? a) (var x : a))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederas (a ->? b) -> a ->? b

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice2

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice3

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder%(op)% =

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder(var f : a ->? b) ((var f : a ->? b) (var x : a))

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederas (a ->? b) * a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Variables -------------------------------------------------------------

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

01996e191c1a9a2251abf7740124b73bde771472Christian Maeder%% Sentences -------------------------------------------------------------

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederforall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice2)%

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice3)%

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maedertwice = (\ (f)(x : a) . f (f x) as (a ->? b) -> a ->? b)

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice)%

c7041924e85535e80c7c08699cb308071d7010beChristian Maedertwice f x = f (f x)

c81507d35d11b2eedf7425a3bb52bceec3224532Christian Maeder%% Diagnostics -----------------------------------------------------------

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 1.6, is type variable 'a'

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

5dca8f36562463e6f691d4d50efe5716d5299801Christian Maeder### Hint 9.20, not a class 'a'