Idris2/tests/idris2/eta001/Issue1370.idr

15 lines
242 B
Idris
Raw Normal View History

identity : (a : Type) -> a -> a
identity a = id
identityL :
(a, b : Type )
-> (f : a -> b)
-> (identity b) . f = f
identityL a b f = Refl
identityR :
(a, b : Type )
-> (f : a -> b)
-> f = (identity b) . f
identityR a b f = Refl