| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Category.Path
Contents
Description
category of paths over morphisms.
Synopsis
- data Path (m :: Type -> Type -> Type) x y where
- toOp2Path :: forall (m :: Type -> Type -> Type) x y. Morphism m => Path m x y -> Path (Op2 m) y x
- fromOp2Path :: forall (m :: Type -> Type -> Type) x y. Morphism m => Path (Op2 m) x y -> Path m y x
- compose :: Category m => Path m x y -> m x y
- mPath :: Morphism m => m x y -> Path m x y
- reverse :: (Morphism m, Morphism f) => (forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u) -> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x
- pthFoldr :: (forall x y. m x y -> f x -> f y) -> f a -> Path m a b -> f b
- pthLength :: forall (m :: Type -> Type -> Type) x y. Path m x y -> N
Path
data Path (m :: Type -> Type -> Type) x y where Source #
paths over morphisms.
Constructors
| IdPath :: forall (m :: Type -> Type -> Type) x. Struct (ObjectClass m) x -> Path m x x | |
| (:.) :: forall (m :: Type -> Type -> Type) y1 y x. m y1 y -> Path m x y1 -> Path m x y infixr 9 |
Instances
toOp2Path :: forall (m :: Type -> Type -> Type) x y. Morphism m => Path m x y -> Path (Op2 m) y x Source #
the opposite path.
fromOp2Path :: forall (m :: Type -> Type -> Type) x y. Morphism m => Path (Op2 m) x y -> Path m y x Source #
from the opposite path.
reverse :: (Morphism m, Morphism f) => (forall u. Struct (ObjectClass m) u -> Struct (ObjectClass f) u) -> (forall u v. m u v -> f v u) -> Path m x y -> Path f y x Source #
reversing a path given by the formal inverse function.