Copyright	(c) Erich Gut
License	BSD3
Maintainer	zerich.gut@gmail.com
Safe Haskell	None
Language	Haskell2010

OAlg.Category.Dualisable

Contents

Dualisable
Dualisable Pairing
Proposition

Description

generalized duality for categories.

Synopsis

class (ReflexiveG r c o d, Transformable1 o r) => DualisableG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where
- toDualG :: Struct r x -> c (d x) (d (o x))
- fromDualG :: Struct r x -> c (d (o x)) (d x)
data DualityG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where
- DualityG :: forall r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type). DualisableG r c o d => DualityG r c o d
class DualisableG r (->) o Id => DualisableGId r (o :: Type -> Type)
class DualisableG r (->) o Pnt => DualisableGPnt r (o :: Type -> Type)
class (Category c, Transformable r (ObjectClass c)) => ReflexiveG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where
- reflG :: Struct r x -> Inv2 c (d x) (d (o (o x)))
reflG' :: forall r (c :: Type -> Type -> Type) o d q x. ReflexiveG r c o d => q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x)))
toDualG' :: DualisableG r c o d => q c o d -> Struct r x -> c (d x) (d (o x))
tauO :: Transformable1 o s => Struct s x -> Struct s (o x)
class (ReflexiveG r c o a, ReflexiveG r c o b, Transformable1 o r) => DualisableGPair r (c :: Type -> Type -> Type) (o :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type) where
- toDualGLft :: Struct r x -> c (a x) (b (o x))
- toDualGRgt :: Struct r x -> c (b x) (a (o x))
- fromDualGLft :: Struct r x -> c (b (o x)) (a x)
- fromDualGRgt :: Struct r x -> c (a (o x)) (b x)
class DualisableGPair r c o d (Dual1 d) => DualisableGBi r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type)
prpDualisableG :: forall r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) q x. (DualisableG r c o d, EqExt c) => q c o d -> Struct r x -> Statement

Dualisable

class (ReflexiveG r c o d, Transformable1 o r) => DualisableG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where Source #

category c equipped with a duality via a reflection.

Property Let DualisableG r c o d, then for all x and r in Struct r x holds:

toDualG' q r' . toDualG' q r .=. u.
toDualG' q r . v .=. v' . toDualG' q r''.
fromDualG' q r .=. v . toDualG' q r'.

where q is any proxy in q c o d, r' = tau1 r , r'' = tau1 r', Inv2 u v = reflG' q r and Inv2 _ v' = reflG' q r'.

Note The properties above imply that toDualG r and fromDualG r are inverse in c for all x and r in Struct r x and hence establish a duality within r structured types.

Minimal complete definition

toDualG

Methods

toDualG :: Struct r x -> c (d x) (d (o x)) Source #

fromDualG :: Struct r x -> c (d (o x)) (d x) Source #

Instances

Instances details

DualisableG OrtX EqualExtOrt Op Id Source #
Instance details Defined in OAlg.Category.Dualisable Methods toDualG :: Struct OrtX x -> EqualExtOrt (Id x) (Id (Op x)) Source # fromDualG :: Struct OrtX x -> EqualExtOrt (Id (Op x)) (Id x) Source #
DualisableG OrtX EqualExtOrt Op Pnt Source #
Instance details Defined in OAlg.Category.Dualisable Methods toDualG :: Struct OrtX x -> EqualExtOrt (Pnt x) (Pnt (Op x)) Source # fromDualG :: Struct OrtX x -> EqualExtOrt (Pnt (Op x)) (Pnt x) Source #
(Transformable r Type, TransformableOp r) => DualisableG r (->) Op Id Source #
Instance details Defined in OAlg.Category.Dualisable Methods toDualG :: Struct r x -> Id x -> Id (Op x) Source # fromDualG :: Struct r x -> Id (Op x) -> Id x Source #
(Transformable r Type, TransformableOp r, Transformable r FbrOrt) => DualisableG r (->) Op Rt Source #
Instance details Defined in OAlg.Category.Dualisable Methods toDualG :: Struct r x -> Rt x -> Rt (Op x) Source # fromDualG :: Struct r x -> Rt (Op x) -> Rt x Source #
(Transformable r Type, TransformableOp r) => DualisableG r (->) Op Pnt Source #
Instance details Defined in OAlg.Category.Dualisable Methods toDualG :: Struct r x -> Pnt x -> Pnt (Op x) Source # fromDualG :: Struct r x -> Pnt (Op x) -> Pnt x Source #

data DualityG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where Source #

attest of being DualisableG.

Constructors

DualityG :: forall r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type). DualisableG r c o d => DualityG r c o d

class DualisableG r (->) o Id => DualisableGId r (o :: Type -> Type) Source #

helper class to avoid undecidable instances.

Instances

Instances details

(TransformableType r, TransformableOp r) => DualisableGId r Op Source #
Instance details Defined in OAlg.Category.Dualisable

class DualisableG r (->) o Pnt => DualisableGPnt r (o :: Type -> Type) Source #

helper class to avoid undecidable instances.

Instances

Instances details

(TransformableType r, TransformableOp r) => DualisableGPnt r Op Source #
Instance details Defined in OAlg.Category.Dualisable

class (Category c, Transformable r (ObjectClass c)) => ReflexiveG r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) where Source #

category c equipped with a reflection on a subset of ObjectClass c given by r.

Methods

reflG :: Struct r x -> Inv2 c (d x) (d (o (o x))) Source #

Instances

Instances details

ReflexiveG OrtX EqualExtOrt Op Id Source #
Instance details Defined in OAlg.Category.Dualisable Methods reflG :: Struct OrtX x -> Inv2 EqualExtOrt (Id x) (Id (Op (Op x))) Source #
ReflexiveG OrtX EqualExtOrt Op Pnt Source #
Instance details Defined in OAlg.Category.Dualisable Methods reflG :: Struct OrtX x -> Inv2 EqualExtOrt (Pnt x) (Pnt (Op (Op x))) Source #
Transformable r Type => ReflexiveG r (->) Op Id Source #
Instance details Defined in OAlg.Category.Dualisable Methods reflG :: Struct r x -> Inv2 (->) (Id x) (Id (Op (Op x))) Source #
Transformable r Type => ReflexiveG r (->) Op Rt Source #
Instance details Defined in OAlg.Category.Dualisable Methods reflG :: Struct r x -> Inv2 (->) (Rt x) (Rt (Op (Op x))) Source #
Transformable r Type => ReflexiveG r (->) Op Pnt Source #
Instance details Defined in OAlg.Category.Dualisable Methods reflG :: Struct r x -> Inv2 (->) (Pnt x) (Pnt (Op (Op x))) Source #

reflG' :: forall r (c :: Type -> Type -> Type) o d q x. ReflexiveG r c o d => q c o d -> Struct r x -> Inv2 c (d x) (d (o (o x))) Source #

prefixing a proxy.

toDualG' :: DualisableG r c o d => q c o d -> Struct r x -> c (d x) (d (o x)) Source #

prefixing a proxy.

tauO :: Transformable1 o s => Struct s x -> Struct s (o x) Source #

propagating the s structure to o.

Dualisable Pairing

class (ReflexiveG r c o a, ReflexiveG r c o b, Transformable1 o r) => DualisableGPair r (c :: Type -> Type -> Type) (o :: Type -> Type) (a :: Type -> Type) (b :: Type -> Type) where Source #

category c equipped with a duality pairing between a and b via reflections.

Minimal complete definition

toDualGLft, toDualGRgt

Methods

toDualGLft :: Struct r x -> c (a x) (b (o x)) Source #

toDualGRgt :: Struct r x -> c (b x) (a (o x)) Source #

fromDualGLft :: Struct r x -> c (b (o x)) (a x) Source #

fromDualGRgt :: Struct r x -> c (a (o x)) (b x) Source #

class DualisableGPair r c o d (Dual1 d) => DualisableGBi r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) Source #

category c equipped with a duality pairing between d and its dual Dual1 d via reflections.

Proposition

prpDualisableG :: forall r (c :: Type -> Type -> Type) (o :: Type -> Type) (d :: Type -> Type) q x. (DualisableG r c o d, EqExt c) => q c o d -> Struct r x -> Statement Source #

validity according to DualisableG.