git.iko.soy/Idris-dev
on master help sign in
Added `Category Iso` in base
e8253fcSynthetica9
libs/base/Control/Isomorphism.idr+5
compare with master
unifiedsplit
@@ -2,6 +2,7 @@ module Control.Isomorphism
2
2
3import Syntax.PreorderReasoning
3import Syntax.PreorderReasoning
4import Data.Fin
4import Data.Fin
5+import Control.Category
5
6
6%default total
7%default total
7%access public export
8%access public export
@@ -32,6 +33,10 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
32 (from (to x)) ={ fromTo x }=
33 (from (to x)) ={ fromTo x }=
33 x QED)
34 x QED)
34
35
36+Category Iso where
37+ id = isoRefl
38+ (.) = flip isoTrans
39+
35||| Isomorphism is symmetric
40||| Isomorphism is symmetric
36isoSym : Iso a b -> Iso b a
41isoSym : Iso a b -> Iso b a
37isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom
42isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom