@@ -2,6 +2,7 @@ module Control.Isomorphism
22
33import Syntax.PreorderReasoning
44import Data.Fin
5+import Control.Category
56
67%default total
78%access public export
@@ -32,6 +33,10 @@ isoTrans (MkIso to from toFrom fromTo) (MkIso to' from' toFrom' fromTo') =
3233 (from (to x)) ={ fromTo x }=
3334 x QED)
3435
36+Category Iso where
37+ id = isoRefl
38+ (.) = flip isoTrans
39+
3540||| Isomorphism is symmetric
3641isoSym : Iso a b -> Iso b a
3742isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom