ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuvars a : Type; b < a

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuop twice2(f : a ->? b) (x : a) :? b = f (f x);

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuop twice3 : (a ->? b) * a ->? b =

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu \ (f : a ->? b, x : a) . f (f x);

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuop twice : (a ->? b) -> a ->? b = \ (f)(x : a) . f (f x);

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuvars f : a ->? b; x : a

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu. twice f x = f (f x);

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu%% Type Variables --------------------------------------------------------

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiua : Type %(var_1)%

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Manceb < a : Type %(var_2)%

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu%% Assumptions -----------------------------------------------------------

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mancetwice

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance%(op)% =

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu(\ ((var f : a ->? a))((var x : a))

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu . (var f : a ->? a) ((var f : a ->? a) (var x : a)))

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuas (a ->? b) -> a ->? b

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiutwice2

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiu: forall a : Type; b < a : Type . (a ->? b) -> a ->? b

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance%(op)% =

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu\ ((var f : a ->? b))((var x : a))

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu. (var f : a ->? b) ((var f : a ->? b) (var x : a)) as b

0505d91991fe8fa70b82c68f360c518f5b2ef358Francisc Nicolae Bungiutwice3

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance: forall a : Type; b < a : Type . (a ->? b) * a ->? b

c038fcf2030a6cfac7a261dee48a9eb29edb78eaFelix Gabriel Mance%(op)% =

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiu(\ ((var f : a ->? b), (var x : a))

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiu . (var f : a ->? b) ((var f : a ->? b) (var x : a)))

6995877e4e201fcf8bb936066da2d259aed7c008Felix Gabriel Manceas (a ->? b) * a ->? b

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu%% Variables -------------------------------------------------------------

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiuf : a ->? b

8d246de26958f1e8c35714b260b9d85c933c060aFrancisc Nicolae Bungiux : a

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiu%% Sentences -------------------------------------------------------------

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiuforall f : a ->? b; x : a . twice2 f x = (f (f x) as b)

6995877e4e201fcf8bb936066da2d259aed7c008Felix Gabriel Mance %(def_twice2)%

ccb84c1cb43fb0ed70c5bf2d364e671820473ed5Francisc Nicolae Bungiutwice3

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu= ((\ (f : a ->? b, x : a) . f (f x)) as (a ->? b) * a ->? b)

8e1b180fc839e96d7a4f1f63dfc563c75139c683Francisc Nicolae Bungiu %(def_twice3)%

8e1b180fc839e96d7a4f1f63dfc563c75139c683Francisc Nicolae Bungiutwice = ((\ (f)(x : a) . f (f x)) as (a ->? b) -> a ->? b)

8e1b180fc839e96d7a4f1f63dfc563c75139c683Francisc Nicolae Bungiu %(def_twice)%

8e1b180fc839e96d7a4f1f63dfc563c75139c683Francisc Nicolae Bungiutwice f x = f (f x)

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu%% Diagnostics -----------------------------------------------------------

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu### Hint 1.6, is type variable 'a'

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu### Hint 9.7, not a kind 'a ->? b'

dda7065c0c0f383558d7d4e8072969c8c41a8ed7Francisc Nicolae Bungiu### Hint 9.20, not a class 'a'

ed1b8e97e72b2e3e92edaf2eb22a4b5373d705f1Felix Gabriel Mance