2fbe4699ac5d2a8bafe8c0c8aa41e6717d36d5ceChristian Maedervars a : Type; b < a

3daa82a175c7cfabf22455aa77c4beda327404e4Christian 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);

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedervars

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedera : Type %(var_1)%;

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederb < a : Type %(var_2)%

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

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder %(op)% =

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

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

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder as (a ->? b) -> a ->? b

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederop twice2 : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder %(op)% =

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

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

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

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder %(op)% =

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

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

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder as (a ->? b) * a ->? b

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maedervars

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maederf : a ->? b;

01996e191c1a9a2251abf7740124b73bde771472Christian Maederx : a

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice2)%

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. twice3

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice3)%

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

5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder %(def_twice)%

e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederforall a : Type; b < a : Type; f : a ->? b; x : a

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. twice f x = f (f x)

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'