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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian Maeder %[op=

f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder (\ f : a ->? a; x : a

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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian Maeder as (a ->? b) -> a ->? b]%

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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian Maeder %[op=

f7663514e02f6095198371a64e574c50e6ec857aChristian Maeder \ f : a ->? b; x : a

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian 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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian Maeder %[op=

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

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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian 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)

6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder. twice3

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

f55c7ffbcd378316d8547132be02b10c5eb4dfb2Christian Maeder. twice

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

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'

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder### Hint 5.14-5.20,

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maederno kind found for 'a ->? b'

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder expected: {Cpo}

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder found: {Type}

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder### Hint 5.14-5.20,

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maederno kind found for 'a ->? b'

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder expected: {Cppo}

17889a13fbcd155040fa0323ffe82393d53051fcChristian Maeder found: {Type}

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

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