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

OAlg.Data.Variant

Contents

Variant
Disjunctive
Proposition

Description

concept of co- and contra.

Synopsis

data Variant
- = Covariant
- | Contravariant
data Variant2 (v :: Variant) (h :: k -> k1 -> Type) (x :: k) (y :: k1) where
- Covariant2 :: forall {k} {k1} (h :: k -> k1 -> Type) (x :: k) (y :: k1). h x y -> Variant2 'Covariant h x y
- Contravariant2 :: forall {k} {k1} (h :: k -> k1 -> Type) (x :: k) (y :: k1). h x y -> Variant2 'Contravariant h x y
toVariant2 :: Disjunctive2 h => h x y -> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y
vmap2 :: forall t (h :: Type -> Type -> Type) b (v :: Variant) x y. ApplicativeG t h b => Variant2 v h x y -> b (t x) (t y)
amapVariant2 :: forall {k1} {k2} f (x :: k1) (y :: k2) g (v :: Variant). (f x y -> g x y) -> Variant2 v f x y -> Variant2 v g x y
class Disjunctive x where
- variant :: x -> Variant
class Disjunctive2 (h :: k -> k1 -> Type) where
- variant2 :: forall (x :: k) (y :: k1). h x y -> Variant
class (Category c, Disjunctive2 c) => CategoryDisjunctive (c :: Type -> Type -> Type)
class CategoryDisjunctive h => CategoryDualisable (o :: Type -> Type) (h :: Type -> Type -> Type) where
- cToDual :: Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x)
- cFromDual :: Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x
vInv2 :: forall (c :: Type -> Type -> Type) (v :: Variant) x y. CategoryDisjunctive c => Variant2 v (Inv2 c) x y -> Variant2 v (Inv2 c) y x
prpCategoryDisjunctive :: forall (c :: Type -> Type -> Type). (CategoryDisjunctive c, Show2 c) => X (SomeObjectClass c) -> X (SomeCmpb2 c) -> Statement
prpCategoryDualisable :: forall (o :: Type -> Type) (h :: Type -> Type -> Type) q. (CategoryDualisable o h, EqExt h) => q o h -> X (SomeObjectClass h) -> Statement

Variant

data Variant Source #

concept of co- and contravariant.

Constructors

Covariant
Contravariant

Instances

Instances details

Bounded Variant Source #
Instance details Defined in OAlg.Data.Variant Methods minBound :: Variant # maxBound :: Variant #
Enum Variant Source #
Instance details Defined in OAlg.Data.Variant Methods succ :: Variant -> Variant # pred :: Variant -> Variant # toEnum :: Int -> Variant # fromEnum :: Variant -> Int # enumFrom :: Variant -> [Variant] # enumFromThen :: Variant -> Variant -> [Variant] # enumFromTo :: Variant -> Variant -> [Variant] # enumFromThenTo :: Variant -> Variant -> Variant -> [Variant] #
Read Variant Source #
Instance details Defined in OAlg.Data.Variant Methods readsPrec :: Int -> ReadS Variant # readList :: ReadS [Variant] # readPrec :: ReadPrec Variant # readListPrec :: ReadPrec [Variant] #
Show Variant Source #
Instance details Defined in OAlg.Data.Variant Methods showsPrec :: Int -> Variant -> ShowS # show :: Variant -> String # showList :: [Variant] -> ShowS #
Eq Variant Source #
Instance details Defined in OAlg.Data.Variant Methods (==) :: Variant -> Variant -> Bool # (/=) :: Variant -> Variant -> Bool #
Ord Variant Source #
Instance details Defined in OAlg.Data.Variant Methods compare :: Variant -> Variant -> Ordering # (<) :: Variant -> Variant -> Bool # (<=) :: Variant -> Variant -> Bool # (>) :: Variant -> Variant -> Bool # (>=) :: Variant -> Variant -> Bool # max :: Variant -> Variant -> Variant # min :: Variant -> Variant -> Variant #
Validable Variant Source #
Instance details Defined in OAlg.Data.Variant Methods valid :: Variant -> Statement Source #
Multiplicative Variant Source #
Instance details Defined in OAlg.Data.Variant Methods one :: Point Variant -> Variant Source # (*) :: Variant -> Variant -> Variant Source # npower :: Variant -> N -> Variant Source #
Oriented Variant Source #
Instance details Defined in OAlg.Data.Variant Methods orientation :: Variant -> Orientation (Point Variant) Source # start :: Variant -> Point Variant Source # end :: Variant -> Point Variant Source #
EqPoint Variant Source #
Instance details Defined in OAlg.Data.Variant
ShowPoint Variant Source #
Instance details Defined in OAlg.Data.Variant
TypeablePoint Variant Source #
Instance details Defined in OAlg.Data.Variant
ValidablePoint Variant Source #
Instance details Defined in OAlg.Data.Variant
type Point Variant Source #
Instance details Defined in OAlg.Data.Variant type Point Variant = ()

data Variant2 (v :: Variant) (h :: k -> k1 -> Type) (x :: k) (y :: k1) where Source #

concept of co- and contravariant for two parameterized types.

Constructors

Covariant2 :: forall {k} {k1} (h :: k -> k1 -> Type) (x :: k) (y :: k1). h x y -> Variant2 'Covariant h x y
Contravariant2 :: forall {k} {k1} (h :: k -> k1 -> Type) (x :: k) (y :: k1). h x y -> Variant2 'Contravariant h x y

Instances

Instances details

Disjunctive2 (Variant2 v h :: k1 -> k2 -> Type) Source #

Instance details

Defined in OAlg.Data.Variant

Methods

variant2 :: forall (x :: k1) (y :: k2). Variant2 v h x y -> Variant Source #

ApplicativeG Id h c => ApplicativeG Id (Variant2 v h) c Source #

Instance details

Defined in OAlg.Data.Variant

Methods

amapG :: Variant2 v h x y -> c (Id x) (Id y) Source #

ApplicativeG Rt h c => ApplicativeG Rt (Variant2 v h) c Source #

Instance details

Defined in OAlg.Data.Variant

Methods

amapG :: Variant2 v h x y -> c (Rt x) (Rt y) Source #

ApplicativeG Pnt h c => ApplicativeG Pnt (Variant2 v h) c Source #

Instance details

Defined in OAlg.Data.Variant

Methods

amapG :: Variant2 v h x y -> c (Pnt x) (Pnt y) Source #

CategoryDisjunctive h => Category (Variant2 'Covariant h) Source #

Instance details

Defined in OAlg.Data.Variant

Methods

cOne :: Struct (ObjectClass (Variant2 'Covariant h)) x -> Variant2 'Covariant h x x Source #

(.) :: Variant2 'Covariant h y z -> Variant2 'Covariant h x y -> Variant2 'Covariant h x z Source #

Morphism h => Morphism (Variant2 v h) Source #

Instance details

Defined in OAlg.Data.Variant

Associated Types

type ObjectClass (Variant2 v h)
Instance details Defined in OAlg.Data.Variant type ObjectClass (Variant2 v h) = ObjectClass h

Methods

homomorphous :: Variant2 v h x y -> Homomorphous (ObjectClass (Variant2 v h)) x y Source #

domain :: Variant2 v h x y -> Struct (ObjectClass (Variant2 v h)) x Source #

range :: Variant2 v h x y -> Struct (ObjectClass (Variant2 v h)) y Source #

Show2 h => Show2 (Variant2 v h) Source #

Instance details

Defined in OAlg.Data.Variant

Methods

show2 :: Variant2 v h a b -> String Source #

(HomAdditive h, Disjunctive2 h) => HomAdditive (Variant2 v h) Source #

Instance details

Defined in OAlg.Hom.Additive

HomDistributiveDisjunctive h => HomDistributive (Variant2 'Covariant h) Source #

Instance details

Defined in OAlg.Hom.Distributive

(HomFibred h, Disjunctive2 h) => HomFibred (Variant2 v h) Source #

Instance details

Defined in OAlg.Hom.Fibred

HomFibredOrientedDisjunctive h => HomFibredOriented (Variant2 'Covariant h) Source #

Instance details

Defined in OAlg.Hom.FibredOriented

HomMultiplicativeDisjunctive h => HomMultiplicative (Variant2 'Covariant h) Source #

Instance details

Defined in OAlg.Hom.Multiplicative

HomOrientedDisjunctive h => HomOriented (Variant2 'Covariant h) Source #

Instance details

Defined in OAlg.Hom.Oriented.Definition

Show (h x y) => Show (Variant2 v h x y) Source #

Instance details

Defined in OAlg.Data.Variant

Methods

showsPrec :: Int -> Variant2 v h x y -> ShowS #

show :: Variant2 v h x y -> String #

showList :: [Variant2 v h x y] -> ShowS #

(Disjunctive2 h, Validable (h x y)) => Validable (Variant2 v h x y) Source #

Instance details

Defined in OAlg.Data.Variant

Methods

valid :: Variant2 v h x y -> Statement Source #

type ObjectClass (Variant2 v h) Source #

Instance details

Defined in OAlg.Data.Variant

type ObjectClass (Variant2 v h) = ObjectClass h

toVariant2 :: Disjunctive2 h => h x y -> Either2 (Variant2 'Contravariant h) (Variant2 'Covariant h) x y Source #

mapping to Variant2 for a Disjunctive2 h.

vmap2 :: forall t (h :: Type -> Type -> Type) b (v :: Variant) x y. ApplicativeG t h b => Variant2 v h x y -> b (t x) (t y) Source #

application on Variant2.

amapVariant2 :: forall {k1} {k2} f (x :: k1) (y :: k2) g (v :: Variant). (f x y -> g x y) -> Variant2 v f x y -> Variant2 v g x y Source #

mapping the Variant2 by preserving the variance.

Disjunctive

class Disjunctive x where Source #

object having an associated variant.

Methods

variant :: x -> Variant Source #

Instances

Instances details

Disjunctive2 h => Disjunctive (Path h x y) Source #
Instance details Defined in OAlg.Data.Variant Methods variant :: Path h x y -> Variant Source #
Disjunctive (HomCo m s o x y) Source #
Instance details Defined in OAlg.Data.HomCo Methods variant :: HomCo m s o x y -> Variant Source #
Disjunctive (HomDisj s o h x y) Source #
Instance details Defined in OAlg.Hom.Definition Methods variant :: HomDisj s o h x y -> Variant Source #
Disjunctive (SHom r s o h x y) Source #
Instance details Defined in OAlg.Category.SDuality Methods variant :: SHom r s o h x y -> Variant Source #
Disjunctive (SMorphism r s o h x y) Source #
Instance details Defined in OAlg.Category.SDuality Methods variant :: SMorphism r s o h x y -> Variant Source #

class Disjunctive2 (h :: k -> k1 -> Type) where Source #

two parameterized object having a associated variant.

Minimal complete definition

Nothing

Methods

variant2 :: forall (x :: k) (y :: k1). h x y -> Variant Source #

default variant2 :: forall (x :: k) (y :: k1). Disjunctive (h x y) => h x y -> Variant Source #

Instances

Instances details

CategoryDisjunctive h => Disjunctive2 (Inv2 h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Data.Variant Methods variant2 :: Inv2 h x y -> Variant Source #
Disjunctive2 h => Disjunctive2 (Path h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Data.Variant Methods variant2 :: Path h x y -> Variant Source #
Disjunctive2 h => Disjunctive2 (Sub s h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Data.Variant Methods variant2 :: Sub s h x y -> Variant Source #
Disjunctive2 (HomCo m s o :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Data.HomCo Methods variant2 :: HomCo m s o x y -> Variant Source #
Disjunctive2 (HomDisj s o h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Hom.Definition Methods variant2 :: HomDisj s o h x y -> Variant Source #
Disjunctive2 (SHom r s o h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Category.SDuality Methods variant2 :: SHom r s o h x y -> Variant Source #
Disjunctive2 (SMorphism r s o h :: Type -> Type -> Type) Source #
Instance details Defined in OAlg.Category.SDuality Methods variant2 :: SMorphism r s o h x y -> Variant Source #
Disjunctive2 (Variant2 v h :: k1 -> k2 -> Type) Source #
Instance details Defined in OAlg.Data.Variant Methods variant2 :: forall (x :: k1) (y :: k2). Variant2 v h x y -> Variant Source #

class (Category c, Disjunctive2 c) => CategoryDisjunctive (c :: Type -> Type -> Type) Source #

disjunctive category.

Properties Let CategoryDisjunctive c, then holds:

For all x and s in Struct (ObjectClass c) x holds: variant2 (cOne s) == Covariant.
For all x, y, z, f in c y z and g in c x y holds: variant2 (f . g) == variant2 f * variant2 g.

Instances

Instances details

CategoryDisjunctive c => CategoryDisjunctive (Inv2 c) Source #
Instance details Defined in OAlg.Data.Variant
(Morphism h, Disjunctive2 h) => CategoryDisjunctive (Path h) Source #
Instance details Defined in OAlg.Data.Variant
(CategoryDisjunctive c, TransformableObjectClass s c) => CategoryDisjunctive (Sub s c) Source #
Instance details Defined in OAlg.Data.Variant
CategoryDisjunctive (HomCo m s o) Source #
Instance details Defined in OAlg.Data.HomCo
Morphism h => CategoryDisjunctive (HomDisj s o h) Source #
Instance details Defined in OAlg.Hom.Definition
Morphism h => CategoryDisjunctive (SHom r s o h) Source #
Instance details Defined in OAlg.Category.SDuality

class CategoryDisjunctive h => CategoryDualisable (o :: Type -> Type) (h :: Type -> Type -> Type) where Source #

disjunctive category admitting duality morphisms.

Property Let CategoryDualisable o h, then for all x and s in Struct ('ObjectClass h) xholds:

f . t .=. cOne (domain t).
t . f .=. cOne (domain f).

where Contravariant2 t = cToDual s and Contravariant2 f = cFromDual s.

Methods

cToDual :: Struct (ObjectClass h) x -> Variant2 'Contravariant h x (o x) Source #

cFromDual :: Struct (ObjectClass h) x -> Variant2 'Contravariant h (o x) x Source #

Instances

Instances details

(Morphism h, TransformableGRefl o s) => CategoryDualisable o (HomDisj s o h) Source #
Instance details Defined in OAlg.Hom.Definition Methods cToDual :: Struct (ObjectClass (HomDisj s o h)) x -> Variant2 'Contravariant (HomDisj s o h) x (o x) Source # cFromDual :: Struct (ObjectClass (HomDisj s o h)) x -> Variant2 'Contravariant (HomDisj s o h) (o x) x Source #
(Morphism h, TransformableGRefl o s) => CategoryDualisable o (SHom r s o h) Source #
Instance details Defined in OAlg.Category.SDuality Methods cToDual :: Struct (ObjectClass (SHom r s o h)) x -> Variant2 'Contravariant (SHom r s o h) x (o x) Source # cFromDual :: Struct (ObjectClass (SHom r s o h)) x -> Variant2 'Contravariant (SHom r s o h) (o x) x Source #

vInv2 :: forall (c :: Type -> Type -> Type) (v :: Variant) x y. CategoryDisjunctive c => Variant2 v (Inv2 c) x y -> Variant2 v (Inv2 c) y x Source #

the inverse Variant2.

Proposition

prpCategoryDisjunctive :: forall (c :: Type -> Type -> Type). (CategoryDisjunctive c, Show2 c) => X (SomeObjectClass c) -> X (SomeCmpb2 c) -> Statement Source #

validity according to CategoryDisjunctive.

prpCategoryDualisable :: forall (o :: Type -> Type) (h :: Type -> Type -> Type) q. (CategoryDualisable o h, EqExt h) => q o h -> X (SomeObjectClass h) -> Statement Source #

validity according to CategoryDualisable.