| Copyright | (c) Erich Gut |
|---|---|
| License | BSD3 |
| Maintainer | zerich.gut@gmail.com |
| Safe Haskell | None |
| Language | Haskell2010 |
OAlg.Entity.Slice.Sliced
Synopsis
- class (Entity1 i, Singleton1 i, Oriented c) => Sliced (i :: Type -> Type) c where
- slicePoint :: i c -> Point c
- sliceIndex :: Sliced i x => q i x -> i x
- class (HomOrientedDisjunctive h, Transformable (ObjectClass h) (Sld i)) => HomSlicedOriented (i :: Type -> Type) (h :: Type -> Type -> Type)
- data Sld (i :: Type -> Type)
- sliceIndexDomain :: Homomorphous (Sld i) x y -> i x
- sliceIndexRange :: Homomorphous (Sld i) x y -> i y
- sldHom :: forall (i :: Type -> Type) h q x y. HomSlicedOriented i h => q i -> h x y -> Homomorphous (Sld i) x y
- toDualOpOrtSld :: forall (i :: Type -> Type) x. Sliced i x => Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
- toDualOpOrtSld' :: forall (i :: Type -> Type) x q. Sliced i x => q i -> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x)
- type HomSlicedMultiplicative (i :: Type -> Type) (h :: Type -> Type -> Type) = (HomSlicedOriented i h, HomMultiplicativeDisjunctive h)
- toDualOpMltSld :: forall (i :: Type -> Type) x. (Sliced i x, Multiplicative x) => Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
- toDualOpMltSld' :: forall (i :: Type -> Type) x q. (Sliced i x, Multiplicative x) => q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x)
- type HomSlicedDistributive (i :: Type -> Type) (h :: Type -> Type -> Type) = (HomSlicedOriented i h, HomDistributiveDisjunctive h)
- toDualOpDstSld :: forall (i :: Type -> Type) x. (Sliced i x, Distributive x) => Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
- toDualOpDstSld' :: forall (i :: Type -> Type) x q. (Sliced i x, Distributive x) => q i -> Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x)
- prpHomSlicedOriented :: forall (i :: Type -> Type) h q x y. (HomSlicedOriented i h, Show2 h) => q i -> h x y -> Statement
Sliced
class (Entity1 i, Singleton1 i, Oriented c) => Sliced (i :: Type -> Type) c where Source #
Slicing Oriented structures at a distinguished Point, given by the type of the index
i.
Note The constraint Singleton1 ii c.
sliceIndex :: Sliced i x => q i x -> i x Source #
the slice index according to the proxy type.
Hom
Oriented
class (HomOrientedDisjunctive h, Transformable (ObjectClass h) (Sld i)) => HomSlicedOriented (i :: Type -> Type) (h :: Type -> Type -> Type) Source #
homomorphisms between Sliced structures, i.e homomorphisms between Oriented structures where
pmap preserves the distinguished point.
Property Let HomSlicedOriented i h
- For all
x,yandhinh x yholds:pmaph px==pypx =,slicePoint$sliceIndexDomain$sldHomq hpy =andslicePoint$sliceIndexRange$sldHomq hqis any proxy inq i.
Instances
| (CategoryDisjunctive h, HomSlicedOriented i h) => HomSlicedOriented i (Inv2 h) Source # | |
Defined in OAlg.Entity.Slice.Sliced | |
| (TransformableOrt s, TransformableType s, TransformableOp s) => HomSlicedOriented i (Sub (s, Sld i) (HomDisjEmpty s Op)) Source # | |
Defined in OAlg.Entity.Slice.Sliced | |
| (TransformableOrt s, TransformableType s, TransformableOp s) => HomSlicedOriented i (Sub (s, Sld i) (IsoO s Op)) Source # | |
Defined in OAlg.Entity.Slice.Sliced | |
| (Transformable s Ort, TransformableOp (s, Sld i)) => HomSlicedOriented i (HomDisjEmpty (s, Sld i) Op) Source # | |
Defined in OAlg.Entity.Slice.Sliced | |
| Attestable k => HomSlicedOriented (Free k) (Sub (Dst, SldFr) (HomDisjEmpty Dst Op)) Source # | |
Defined in OAlg.Entity.Slice.Free | |
data Sld (i :: Type -> Type) Source #
type index for Sliced structures.
Instances
sliceIndexDomain :: Homomorphous (Sld i) x y -> i x Source #
the slice index for the domain.
sliceIndexRange :: Homomorphous (Sld i) x y -> i y Source #
the slice index for the range.
sldHom :: forall (i :: Type -> Type) h q x y. HomSlicedOriented i h => q i -> h x y -> Homomorphous (Sld i) x y Source #
the induced homomorphous structure.
toDualOpOrtSld :: forall (i :: Type -> Type) x. Sliced i x => Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x) Source #
toDualOpOrtSld' :: forall (i :: Type -> Type) x q. Sliced i x => q i -> Variant2 'Contravariant (IsoO (Ort, Sld i) Op) x (Op x) Source #
Multiplicative
type HomSlicedMultiplicative (i :: Type -> Type) (h :: Type -> Type -> Type) = (HomSlicedOriented i h, HomMultiplicativeDisjunctive h) Source #
disjunctive multiplicative homomorphism respecting the slice structure.
toDualOpMltSld :: forall (i :: Type -> Type) x. (Sliced i x, Multiplicative x) => Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x) Source #
contravariant isomorphism on Sliced Multiplicative structures.
toDualOpMltSld' :: forall (i :: Type -> Type) x q. (Sliced i x, Multiplicative x) => q i -> Variant2 'Contravariant (IsoO (Mlt, Sld i) Op) x (Op x) Source #
contravariant isomorphism on Sliced Multiplicative structures according to the proxy type.
Distributive
type HomSlicedDistributive (i :: Type -> Type) (h :: Type -> Type -> Type) = (HomSlicedOriented i h, HomDistributiveDisjunctive h) Source #
disjunctive distributive homomorphism respecting the slice structure.
toDualOpDstSld :: forall (i :: Type -> Type) x. (Sliced i x, Distributive x) => Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x) Source #
contravariant isomorphism on Sliced Distributive structures.
toDualOpDstSld' :: forall (i :: Type -> Type) x q. (Sliced i x, Distributive x) => q i -> Variant2 'Contravariant (IsoO (Dst, Sld i) Op) x (Op x) Source #
contravariant isomorphism on Sliced Distributive structures according to the proxy type.
Proposition
prpHomSlicedOriented :: forall (i :: Type -> Type) h q x y. (HomSlicedOriented i h, Show2 h) => q i -> h x y -> Statement Source #
validity according to HomSlicedOriented.