| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Data.HomCo
Contents
Description
mapping between an object m in m x and its co-object, where Dual1 m_ ~ m
Synopsis
- data HomCo (m :: Type -> Type) s (o :: Type -> Type) x y
- toCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> MorCo m s o (o (m x)) (m (o x))
- fromCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> MorCo m s o (m (o x)) (o (m x))
- sHomCo :: forall s (o :: Type -> Type) (m :: Type -> Type) x y. SHom s s o (MorCo m s o) x y -> HomCo m s o x y
- newtype PathCo (m :: Type -> Type) s (o :: Type -> Type) x y = PathCo (Path (SMorphism s s o (MorCo m s o)) x y)
- rdcCoToFromCo :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y)
- rdcCoToFromDual :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y)
- rdcPathCo :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y)
- data MorCo (m :: Type -> Type) s (o :: Type -> Type) x y where
- ToCo :: forall s x1 (m :: Type -> Type) (o :: Type -> Type). (Structure s x1, TransformableG m s s, TransformableG o s s) => MorCo m s o (o (m x1)) (m (o x1))
- FromCo :: forall s x1 (m :: Type -> Type) (o :: Type -> Type). (Structure s x1, TransformableG m s s, TransformableG o s s) => MorCo m s o (m (o x1)) (o (m x1))
- mcoStruct :: forall (m :: Type -> Type) s (o :: Type -> Type) i j x y. MorCo m s o (i (j x)) y -> Struct s x
- class ApplicativeG d (MorCo m s o) c => ApplicativeMorCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type)
- class (Category c, ApplicativeMorCo d m s o c, TransformableG m s s, TransformableG o s s, TransformableG d s (ObjectClass c)) => FunctorialHomCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type)
- data FunctorHomCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type) where
- FunctorHomCo :: forall (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type). FunctorialHomCo d m s o c => FunctorHomCo d m s o c
- isoCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x))
- type IsoCo (m :: Type -> Type) s (o :: Type -> Type) = Inv2 (HomCo m s o)
- xscHomCo :: forall (o :: Type -> Type) s (m :: Type -> Type). TransformableG o s s => N -> X (SomeObjectClass (HomCo m s o)) -> X (SomeMorphism (MorCo m s o)) -> X (SomeCmpb2 (HomCo m s o))
- prpFunctorialHomCo :: forall (c :: Type -> Type -> Type) (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) x. EqExt c => FunctorHomCo d m s o c -> Struct s x -> Statement
Category
data HomCo (m :: Type -> Type) s (o :: Type -> Type) x y Source #
homomorphism for applications of objects m over x.
Instances
toCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> MorCo m s o (o (m x)) (m (o x)) Source #
to the co-object.
fromCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> MorCo m s o (m (o x)) (o (m x)) Source #
from the co-cobject.
sHomCo :: forall s (o :: Type -> Type) (m :: Type -> Type) x y. SHom s s o (MorCo m s o) x y -> HomCo m s o x y Source #
functorial projection to HomCo.
newtype PathCo (m :: Type -> Type) s (o :: Type -> Type) x y Source #
rdcCoToFromCo :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y) Source #
rdcCoToFromDual :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y) Source #
reducing a PathCo according to rdcPathSMorphism.
rdcPathCo :: forall (m :: Type -> Type) s (o :: Type -> Type) x y. PathCo m s o x y -> Rdc (PathCo m s o x y) Source #
applying the rules of rdcCoToFromCo and rdcCoToFromDual.
data MorCo (m :: Type -> Type) s (o :: Type -> Type) x y where Source #
morphism to and from the co-cobject.
Constructors
| ToCo :: forall s x1 (m :: Type -> Type) (o :: Type -> Type). (Structure s x1, TransformableG m s s, TransformableG o s s) => MorCo m s o (o (m x1)) (m (o x1)) | |
| FromCo :: forall s x1 (m :: Type -> Type) (o :: Type -> Type). (Structure s x1, TransformableG m s s, TransformableG o s s) => MorCo m s o (m (o x1)) (o (m x1)) |
Instances
| (TransformableDst s, TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeG Id (MorCo Matrix s o) (->) Source # | |||||
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeG Rt (MorCo Matrix s o) (->) Source # | |||||
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeG Pnt (MorCo Matrix s o) (->) Source # | |||||
| Morphism (MorCo m s o) Source # | |||||
Defined in OAlg.Data.HomCo Associated Types
Methods homomorphous :: MorCo m s o x y -> Homomorphous (ObjectClass (MorCo m s o)) x y Source # domain :: MorCo m s o x y -> Struct (ObjectClass (MorCo m s o)) x Source # range :: MorCo m s o x y -> Struct (ObjectClass (MorCo m s o)) y Source # | |||||
| Show2 (MorCo m s o) Source # | |||||
| Show (MorCo m s o x y) Source # | |||||
| type ObjectClass (MorCo m s o) Source # | |||||
Defined in OAlg.Data.HomCo | |||||
mcoStruct :: forall (m :: Type -> Type) s (o :: Type -> Type) i j x y. MorCo m s o (i (j x)) y -> Struct s x Source #
whitness that x is a s structure.
Functor
class ApplicativeG d (MorCo m s o) c => ApplicativeMorCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type) Source #
helper class to avoid undecidable instances.
Instances
| (TransformableDst s, TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeMorCo Id Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeMorCo Rt Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => ApplicativeMorCo Pnt Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
class (Category c, ApplicativeMorCo d m s o c, TransformableG m s s, TransformableG o s s, TransformableG d s (ObjectClass c)) => FunctorialHomCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type) Source #
functorial predicat for HomCo.
Properties Let FunctorialHomCo d s m o cx
and s in Struct s x
amapG(fromCos).amapG(toCos).=.cOneDOMf samapG(toCos).amapG(fromCos).=.cOneDMOf s
where f is anay proxy in q d s m o c.
Instances
| (TransformableDst s, TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => FunctorialHomCo Id Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => FunctorialHomCo Rt Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
| (TransformableGRefl o s, DualisableDistributive s o, TransformableGRefl Matrix s) => FunctorialHomCo Pnt Matrix s o (->) Source # | |
Defined in OAlg.Entity.Matrix.Definition | |
data FunctorHomCo (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type) where Source #
whiteness of being FunctorialHomCo.
Constructors
| FunctorHomCo :: forall (d :: Type -> Type) (m :: Type -> Type) s (o :: Type -> Type) (c :: Type -> Type -> Type). FunctorialHomCo d m s o c => FunctorHomCo d m s o c |
Iso
isoCo :: (TransformableG m s s, TransformableG o s s) => Struct s x -> Variant2 'Contravariant (IsoCo m s o) (m x) (m (o x)) Source #
contravariant isomorphism.
type IsoCo (m :: Type -> Type) s (o :: Type -> Type) = Inv2 (HomCo m s o) Source #
isomorphism for HomCo.
X
xscHomCo :: forall (o :: Type -> Type) s (m :: Type -> Type). TransformableG o s s => N -> X (SomeObjectClass (HomCo m s o)) -> X (SomeMorphism (MorCo m s o)) -> X (SomeCmpb2 (HomCo m s o)) Source #
random variable for some composable HomCos.