1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskivars a : Type; b < a

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiop twice2(f : a ->? b) (x : a) :? b = f (f x);

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskiop twice3 : (a ->? b) * a ->? b =

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

f7819aa9d183836144a98c70d4fa7d65e31cb513Till Mossakowskiop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maedervars f : a ->? b; x : a

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

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowski%% Type Variables --------------------------------------------------------

1b05bdb88b90d3c947351f262d7ae7d68f0a4a6fTill Mossakowskia : Type %(var_1)%

e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowskib < a : Type %(var_2)%

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%% Assumptions -----------------------------------------------------------

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedertwice

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%(op)% =

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederas (a ->? b) -> a ->? b

c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian Maedertwice2

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%(op)% =

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

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

e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowskitwice3

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%(op)% =

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

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederas (a ->? b) * a ->? b

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%% Variables -------------------------------------------------------------

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederf : a ->? b

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederx : a

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%% Sentences -------------------------------------------------------------

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder %(def_twice2)%

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedertwice3

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder %(def_twice3)%

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedertwice = ((\ (f)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder %(def_twice)%

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedertwice f x = f (f x)

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder%% Diagnostics -----------------------------------------------------------

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder### Hint 1.6, is type variable 'a'

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

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder### Hint 9.20, not a class 'a'

95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder