Make Iso a record
This makes it possible to run an Iso on a value directly without
matching on it.
commit1c0bf464f7208915e202a0909e5cc5a2f713a87c
authorhowtonotwin <rasheeqhere@gmail.com>
dateThu 29 Mar 2018, 13:32 (9 years ago)
parent958d89e
libs/base/Control/Isomorphism.idr+6−6
@@ -8,12 +8,12 @@ import Control.Category
88%access public export
99
1010||| An isomorphism between two types
11−data Iso : Type -> Type -> Type where
12− MkIso : (to : a -> b) ->
13− (from : b -> a) ->
14− (toFrom : (y : b) -> to (from y) = y) ->
15− (fromTo : (x : a) -> from (to x) = x) ->
16− Iso a b
11+record Iso a b where
12+ constructor MkIso
13+ to : a -> b
14+ from : b -> a
15+ toFrom : (y : b) -> to (from y) = y
16+ fromTo : (x : a) -> from (to x) = x
1717
1818-- Isomorphism properties
1919
test/disambig002/disambig002.idr−5
@@ -19,11 +19,6 @@ Unique0 = Unique
1919Unique1 : (t0 -> Type) -> Type
2020Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)
2121
22−namespace Iso
23−
24− from : {A, B : Type} -> Iso A B -> (B -> A)
25− from (MkIso to from toFrom fromTo) = from
26−
2722namespace Fin
2823
2924 ||| 'Tail' of a finite function