020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettvars a : Type; b : Type

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimbletttypes i a b, Inj a b < a -> b

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowskivars a : Type; b < a

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettop twice : (a ->? b) -> (a ->? b)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettvars f : a ->? b; x : a

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett. twice f x = f (f x);

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettvars a : Type; b : Type

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimbletttype Inj a b = {f : a -> b . forall x, y : a . f x = f y => x = y}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettvars a, b : Type; a < b

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettop down : b ->? a

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettvars y : b; x : a

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett. down y = x;

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettop up : a -> b

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblett. down (up x : b) = x

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett. def (down (y : b) : a) => up (down y : a) = y;

1aef7e013543ce13074e14d093b1613e67cabc6aAndy Gimblettvars c : Type; b < c

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettvar x : a

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett. up (up x : b) = (up x : c)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett. up (x : a) = (x : b);

1aef7e013543ce13074e14d093b1613e67cabc6aAndy Gimblettvars c, d, e, f : Type; c < e; d < f

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettforall f : e -> f . (up f : e ->? f) = \ x : e . f x;

9ebbce450fb242e1a346f9f89367d8c46fcb2ec8Andy Gimblettforall f : e ->? d . (up f : c ->? f) = \ x : c . up (f (up x));

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblettforall x : c; y : d . (up (x, y) : e * f) = (up x, up y);

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimbletttypes

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettInj : Type -> Type -> Type;

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimbletti : Type -> Type -> Type

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimbletttypes

567db7182e691cce5816365d8c912d09ffe92f86Andy GimblettInj < __->__;

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimbletti < __->__

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblettvars

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimbletta < b : Type %(var_53)%;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettb < c : Type %(var_99)%;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettc < e : Type %(var_128)%;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettd < f : Type %(var_129)%;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblette : Type %(var_126)%;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettf : Type %(var_127)%

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettop down : forall b : Type; a < b : Type . b ->? a %(op)%

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettop twice : forall a : Type; b < a : Type . (a ->? b) -> a ->? b

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett %(op)%

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettop up : forall b : Type; a < b : Type . a -> b %(op)%

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettvars

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettf : a ->? b;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettx : a;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimbletty : b

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a : Type; b < a : Type; f : a ->? b; x : a

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. twice f x = f (f x)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; b : Type; x : a; y : b . down y = x

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; b : Type; x : a . down (up x : b) = x

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; b : Type; y : b

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. def (down (y : b) : a) => up (down y : a) = y

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; b < c : Type; c : Type; x : a

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. up (up x : b) = (up x : c)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; b < c : Type; x : a . up (x : a) = (x : b)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall a < b : Type; e : Type; f : Type; f : e -> f

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. (up f : e ->? f) = \ (x : a) : e . f x

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimbletta < b : Type; c < e : Type; d < f : Type; e : Type; f : Type;

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettf : e ->? d

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. (up f : c ->? f) = \ (x : a) : c . up (f (up x))

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblettforall c < e : Type; d < f : Type; e : Type; f : Type; x : c; y : d

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett. (up (x, y) : e * f) = (up x, up y)

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 1.6, is type variable 'a'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 1.15, is type variable 'b'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 2.8, rebound type variable 'a'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 2.10, rebound type variable 'b'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 3.6, is type variable 'a'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 3.6, rebound type variable 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 3.15, rebound type variable 'b'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 6.7, not a kind 'a ->? b'

54eb3ebb6d142adedee7ce8b8f4d51d554b3b9e0Andy Gimblett### Hint 6.19, not a class 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 9.6, is type variable 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 9.6, rebound type variable 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 9.15, is type variable 'b'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 9.15, rebound type variable 'b'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 10.17, rebound variable 'f'

da955132262baab309a50fdffe228c9efe68251dCui Jian### Hint 10.37, not a class 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 10.40, not a class 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 10.36, rebound variable 'x'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 10.6, redeclared type 'Inj'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 10.22, repeated supertype '__->__'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 12.6, is type variable 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 12.6, rebound type variable 'a'

61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett### Hint 12.9, is type variable 'b'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 12.9, rebound type variable 'b'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 12.18, rebound type variable 'a'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 14.7, not a class 'b'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 14.13, not a class 'a'

1c7c4d95775a8ad5f7373e5cf0bad86f8301c56cAndy Gimblett### Hint 14.12, rebound variable 'x'

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett### Hint 21.6, is type variable 'c'

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett### Hint 21.15, rebound type variable 'b'

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett### Hint 23.6, not a class 'a'

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett### Hint 23.5, rebound variable 'x'

aa0d5f8be9950e788884f7431cf4cb7bee74788cAndy Gimblett### Hint 27.6, rebound type variable 'c'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 27.18, rebound type variable 'c'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 27.25, rebound type variable 'd'

69b3701bf367eacfedd3efef1b95f697228e592aAndy Gimblett### Hint 28.9, not a class 'e'

69b3701bf367eacfedd3efef1b95f697228e592aAndy Gimblett### Hint 28.9, not a class 'f'

69b3701bf367eacfedd3efef1b95f697228e592aAndy Gimblett### Hint 28.8, rebound variable 'f'

69b3701bf367eacfedd3efef1b95f697228e592aAndy Gimblett### Hint 28.39, rebound variable 'x'

69b3701bf367eacfedd3efef1b95f697228e592aAndy Gimblett### Hint 29.9, not a kind 'e ->? d'

8400689f5338073e0f5fe1ae9a1cdb658c2db83bAndy Gimblett### Hint 29.8, rebound variable 'f'

8400689f5338073e0f5fe1ae9a1cdb658c2db83bAndy Gimblett### Hint 29.40, rebound variable 'x'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 30.9, not a class 'c'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 30.8, rebound variable 'x'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 30.15, not a class 'd'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett### Hint 30.14, rebound variable 'y'

afc52bfaabee38c4d55cee9f35b1a0028ba3854aAndy Gimblett