2fbe4699ac5d2a8bafe8c0c8aa41e6717d36d5ceChristian Maedervars a : Type; b < a

a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederop twice2(f : a ->? b) (x : a) :? b = f (f x);

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maederop twice3 : (a ->? b) * a ->? b =

a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maeder \ (f : a ->? b, x : a) . f (f x);

a59f2017dfc311ece7afcea3e8a3ceceac77ba5aChristian Maederop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

2fbe4699ac5d2a8bafe8c0c8aa41e6717d36d5ceChristian Maedervars f : a ->? b; x : a

f8a1ab8012a1f36060d6ce9b63399fa4a8a2981cChristian Maeder. twice f x = f (f x);

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

384d1098c68ef05b8369b4d6b43733f3d1e1e687Christian Maedera : Type %(var_1)%

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

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

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder %(op)% =

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

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

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

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder %(op)% =

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

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

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

ad187062b0009820118c1b773a232e29b879a2faChristian Maeder %(op)% =

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

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

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

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

01996e191c1a9a2251abf7740124b73bde771472Christian Maederf : a ->? b

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

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

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice2)%

0a907ffb1de8958ba48d229e5f5039141d4499ccChristian Maedertwice3

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice3)%

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian 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'