git.iko.soy/Idris-dev
on master help sign in
Data.Morphisms: add casts between morphisms where possible

The following two `Cast` implementations are included, along with their respective inverse. * `Cast (Endomorphism a) (Morphism a a)` * `Cast (Kleislimorphism m a b) (Morphism a (m b))`

commit48a8923707e2c3e6918e741b784befec5e444d20 authorMichael Morgan <morgan.michael@me.com> dateMon 28 Aug 2017, 22:16 (9 years ago) parentc97bf3f
1 file changed+12
compare with master
unifiedsplit
libs/base/Data/Morphisms.idr+12
libs/base/Data/Morphisms.idr+12
@@ -40,3 +40,15 @@ infixr 1 ~>
4040
4141(~>) : Type -> Type -> Type
4242a ~> b = Morphism a b
43+
44+Cast (Endomorphism a) (Morphism a a) where
45+ cast (Endo f) = Mor f
46+
47+Cast (Morphism a a) (Endomorphism a) where
48+ cast (Mor f) = Endo f
49+
50+Monad m => Cast (Morphism a (m b)) (Kleislimorphism m a b) where
51+ cast (Mor f) = Kleisli f
52+
53+Cast (Kleislimorphism m a b) (Morphism a (m b)) where
54+ cast (Kleisli f) = Mor f