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

OAlg.Entity.Slice.Free

Contents

Description

sliced structures with assigned free Points of some given dimension.

Synopsis

newtype Free (k :: N') c = Free (Any k)
free' :: forall q x (k :: N'). q x -> Any k -> Free k x
freeN :: forall (k :: N') c. Free k c -> N
castFree :: forall (k :: N') x y. Free k x -> Free k y
isFree :: forall (k :: N') c. Sliced (Free k) c => Free k c -> Point c -> Bool
data SomeFree c where
- SomeFree :: forall (k :: N') c. (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c
sfrPoint :: SomeFree x -> Point x
sfrMap :: forall (h :: Type -> Type -> Type) (v :: Variant) x y. HomOrientedSlicedFree h => Variant2 v h x y -> SomeFree x -> SomeFree y
class SlicedFree x where
- slicedFree :: forall (k :: N'). Attestable k => Struct (Sld (Free k)) x
data SldFr
class (HomOrientedDisjunctive h, Transformable (ObjectClass h) SldFr) => HomOrientedSlicedFree (h :: Type -> Type -> Type)
prpHomOrientedSlicedFree :: forall h x y (k :: N'). (HomOrientedSlicedFree h, Show2 h) => h x y -> Any k -> Statement
data SomeFreeSlice (s :: Site) c where
- SomeFreeSlice :: forall (k :: N') c (s :: Site). (Attestable k, Sliced (Free k) c) => Slice s (Free k) c -> SomeFreeSlice s c
slicedFree' :: forall x (k :: N') q. (SlicedFree x, Attestable k) => q x -> Any k -> Struct (Sld (Free k)) x
data DiagramFree (t :: DiagramType) (n :: N') (m :: N') a = DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)
dgfDiagram :: forall (t :: DiagramType) (n :: N') (m :: N') a. DiagramFree t n m a -> Diagram t n m a
dgfMapS :: forall h (t :: DiagramType) x y (n :: N') (m :: N'). (HomOrientedSlicedFree h, t ~ Dual (Dual t)) => h x y -> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y
dgfMapCov :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Covariant h x y -> DiagramFree t n m x -> DiagramFree t n m y
dgfMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Contravariant h x y -> DiagramFree t n m x -> DiagramFree (Dual t) n m y
data SomeFreeSliceDiagram (t :: DiagramType) (n :: N') (m :: N') x where
- SomeFreeSliceKernel :: forall (k :: N') x. (Attestable k, Sliced (Free k) x) => Slice 'From (Free k) x -> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) ('S N0) x
- SomeFreeSliceCokernel :: forall (k :: N') x. (Attestable k, Sliced (Free k) x) => Slice 'To (Free k) x -> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) ('S N0) x
sfsdMapS :: forall h (t :: DiagramType) x y (n :: N') (m :: N'). (HomOrientedSlicedFree h, t ~ Dual (Dual t)) => h x y -> SDualBi (SomeFreeSliceDiagram t n m) x -> SDualBi (SomeFreeSliceDiagram t n m) y
sfsdMapCov :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Covariant h x y -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y
sfsdMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Contravariant h x y -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram (Dual t) n m y
data ConeLiftable s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where
- ConeKernelLiftable :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x. KernelConic Cone d N1 x -> LiftableFree 'Projective x -> ConeLiftable Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) ('S N0) x
- ConeCokernelLiftable :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x. CokernelConic Cone d N1 x -> LiftableFree 'Injective x -> ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) ('S N0) x
cnLiftable :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. ConeLiftable s p d t n m x -> LiftableFree p x
cnlMapS :: forall s (d :: DiagramType -> N' -> N' -> Type -> Type) (p :: Perspective) (t :: DiagramType) x y (n :: N') (m :: N'). (NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => Inv2 (HomFree s) x y -> SDualBi (ConeLiftable s p d t n m) x -> SDualBi (ConeLiftable s p d t n m) y
data LiftableFree (p :: Perspective) x where
- LiftableFree :: forall (p :: Perspective) x. (forall (k :: N'). Any k -> Liftable p (Free k) x) -> LiftableFree p x
liftFree :: forall (p :: Perspective) x (k :: N'). LiftableFree p x -> Any k -> Liftable p (Free k) x
type HomFree s = Sub (s, SldFr) (HomDisjEmpty s Op)
lftFrMapSMlt :: forall (p :: Perspective) x y. p ~ Dual (Dual p) => Inv2 (HomFree Mlt) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
lftFrMapSDst :: forall (p :: Perspective) x y. p ~ Dual (Dual p) => Inv2 (HomFree Dst) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y
class (NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m) => NaturalDiagrammaticFree s (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (m :: N')
type CokernelsLiftableSomeFree = CokernelsG ConeLiftable SomeFreeSliceDiagram N1
type CokernelLiftableSomeFree = CokernelG ConeLiftable SomeFreeSliceDiagram N1
data ConicFreeTip (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where
- ConicFreeTip :: forall (k :: N') x (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (Attestable k, Sliced (Free k) x) => Free k x -> c s p d t n m x -> ConicFreeTip c s p d t n m x
type KernelsSomeFreeFreeTip = KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1
type KernelSomeFreeFreeTip = KernelG (ConicFreeTip Cone) SomeFreeSliceDiagram N1
data KernelSliceFromSomeFreeTip (n :: N') (i :: Type -> Type) c where
- KernelSliceFromSomeFreeTip :: forall (k' :: N') c (i :: Type -> Type) (n :: N'). (Attestable k', Sliced (Free k') c) => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c
toDualOpFreeDst :: (Distributive x, SlicedFree x) => Variant2 'Contravariant (Inv2 (HomFree Dst)) x (Op x)

Free

newtype Free (k :: N') c Source #

index for free points within a Multiplicative structure c.

>>> lengthN (Free attest :: Free N3 c) 3

Constructors

Free (Any k)

Instances

Instances details

Attestable k => NaturalDiagrammaticFree Dst (SliceDiagram (Free k)) N2 N1 Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction
Eq1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods eq1 :: Free k x -> Free k x -> Bool Source #
Show1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods show1 :: Free k x -> String Source #
Attestable k => Singleton1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods unit1 :: Free k x Source #
Validable1 (Free k) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid1 :: Free k x -> Statement Source #
Attestable k => HomSlicedOriented (Free k) (Sub (Dst, SldFr) (HomDisjEmpty Dst Op)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Show (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> Free k c -> ShowS # show :: Free k c -> String # showList :: [Free k c] -> ShowS #
Eq (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods (==) :: Free k c -> Free k c -> Bool # (/=) :: Free k c -> Free k c -> Bool #
Validable (Free k c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: Free k c -> Statement Source #
Attestable k => Transformable (s, SldFr) (Sld (Free k)) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct (Sld (Free k)) x Source #
(Distributive a, XStandardEligibleConeCokernel N1 a, XStandardEligibleConeFactorCokernel N1 a, XStandardEligibleConeKernel N1 a, XStandardEligibleConeFactorKernel N1 a, XStandardSomeFreeSliceFromLiftable a) => Validable (FinitePresentation 'To Free a) Source #
Instance details Defined in OAlg.Data.FinitelyPresentable Methods valid :: FinitePresentation 'To Free a -> Statement Source #

free' :: forall q x (k :: N'). q x -> Any k -> Free k x Source #

k-Free of x, given by the proxy q x.

freeN :: forall (k :: N') c. Free k c -> N Source #

the underlying natural number.

castFree :: forall (k :: N') x y. Free k x -> Free k y Source #

casting between Free types.

isFree :: forall (k :: N') c. Sliced (Free k) c => Free k c -> Point c -> Bool Source #

check for being a free point, i.e. if it is equal to slicePoint.

Definition Let n be in Free n c and p in Point c then we call p of order n if and only if slicePoint i == p.

data SomeFree c where Source #

some free attest.

Constructors

SomeFree :: forall (k :: N') c. (Attestable k, Sliced (Free k) c) => Free k c -> SomeFree c

Instances

Instances details

Show (SomeFree c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> SomeFree c -> ShowS # show :: SomeFree c -> String # showList :: [SomeFree c] -> ShowS #
Eq (SomeFree c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods (==) :: SomeFree c -> SomeFree c -> Bool # (/=) :: SomeFree c -> SomeFree c -> Bool #
Validable (SomeFree c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: SomeFree c -> Statement Source #

sfrPoint :: SomeFree x -> Point x Source #

the given slice point.

sfrMap :: forall (h :: Type -> Type -> Type) (v :: Variant) x y. HomOrientedSlicedFree h => Variant2 v h x y -> SomeFree x -> SomeFree y Source #

mapping of SomeFree.

Sliced Free

class SlicedFree x where Source #

attest for k-free sliced structures.

Methods

slicedFree :: forall (k :: N'). Attestable k => Struct (Sld (Free k)) x Source #

Instances

Instances details

SlicedFree x => SlicedFree (Op x) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods slicedFree :: forall (k :: N'). Attestable k => Struct (Sld (Free k)) (Op x) Source #

data SldFr Source #

SlicedFree structures.

Instances

Instances details

HomOrientedSlicedFree (Inv2 (HomFree Dst)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
HomOrientedSlicedFree (Inv2 (HomFree Mlt)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(TransformableOrt s, TransformableType s, TransformableOp s) => HomOrientedSlicedFree (HomFree s) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree s) x y -> SDualBi (ConeLiftable s p d t n m) x -> SDualBi (ConeLiftable s p d t n m) y Source #
p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree Dst) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #
p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree Mlt) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #
(NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Attestable k => HomSlicedOriented (Free k) (Sub (Dst, SldFr) (HomDisjEmpty Dst Op)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
FunctorialOriented (Sub (Dst, SldFr) (HomDisjEmpty Dst Op)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
FunctorialOriented (Sub (Mlt, SldFr) (HomDisjEmpty Mlt Op)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableAdd s => TransformableAdd (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableDst s => TransformableDst (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableFbr s => TransformableFbr (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableFbrOrt s => TransformableFbrOrt (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableMlt s => TransformableMlt (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableOrt s => TransformableOrt (s, SldFr) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Transformable (s, SldFr) SldFr Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct SldFr x Source #
Transformable s Add => Transformable (s, SldFr) Add Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct Add x Source #
Transformable s Dst => Transformable (s, SldFr) Dst Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct Dst x Source #
Transformable s Fbr => Transformable (s, SldFr) Fbr Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct Fbr x Source #
Transformable s FbrOrt => Transformable (s, SldFr) FbrOrt Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct FbrOrt x Source #
Transformable s Mlt => Transformable (s, SldFr) Mlt Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct Mlt x Source #
Transformable s Ort => Transformable (s, SldFr) Ort Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct Ort x Source #
Attestable k => Transformable (s, SldFr) (Sld (Free k)) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods tau :: Struct (s, SldFr) x -> Struct (Sld (Free k)) x Source #
TransformableObjectClass (Dst, SldFr) (HomDisj Dst Op (HomEmpty Dst)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
TransformableObjectClass (Mlt, SldFr) (HomDisj Mlt Op (HomEmpty Mlt)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
type Structure SldFr x Source #
Instance details Defined in OAlg.Entity.Slice.Free type Structure SldFr x = SlicedFree x

class (HomOrientedDisjunctive h, Transformable (ObjectClass h) SldFr) => HomOrientedSlicedFree (h :: Type -> Type -> Type) Source #

homomorphisms between SlicedFree structures, i.e. homomorphisms between Oriented structures where pmap preserves the k-parameterized slice points.

Property Let HomOrientedSlicedFree h, then for all x, y and h in h x y holds:

For all k holds: pmap h (slicePoint $ free' qx k) == (slicePoint $ free' qy k) where k is in Free k x and qx is any proxy in q x and qy is any proxy in q y.

Instances

Instances details

HomOrientedSlicedFree (Inv2 (HomFree Dst)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
HomOrientedSlicedFree (Inv2 (HomFree Mlt)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(TransformableOrt s, TransformableType s, TransformableOp s) => HomOrientedSlicedFree (HomFree s) Source #
Instance details Defined in OAlg.Entity.Slice.Free

prpHomOrientedSlicedFree :: forall h x y (k :: N'). (HomOrientedSlicedFree h, Show2 h) => h x y -> Any k -> Statement Source #

validity according to HomOrientedSlicedFree.

data SomeFreeSlice (s :: Site) c where Source #

some free point within a Multiplicative structure c.

Constructors

SomeFreeSlice :: forall (k :: N') c (s :: Site). (Attestable k, Sliced (Free k) c) => Slice s (Free k) c -> SomeFreeSlice s c

Instances

Instances details

Show c => Show (SomeFreeSlice s c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> SomeFreeSlice s c -> ShowS # show :: SomeFreeSlice s c -> String # showList :: [SomeFreeSlice s c] -> ShowS #
Validable (SomeFreeSlice s c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: SomeFreeSlice s c -> Statement Source #

slicedFree' :: forall x (k :: N') q. (SlicedFree x, Attestable k) => q x -> Any k -> Struct (Sld (Free k)) x Source #

attest for k-free sliced structures according to the given proxy type.

Diagram Free

data DiagramFree (t :: DiagramType) (n :: N') (m :: N') a Source #

predicate for diagrams with free points.

Constructors

DiagramFree (FinList n (SomeFree a)) (Diagram t n m a)

Instances

Instances details

Diagrammatic DiagramFree Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. DiagramFree t n m x -> Diagram t n m x Source #
NaturalDiagrammaticFree Dst DiagramFree n m Source #
Instance details Defined in OAlg.Entity.Slice.Free
(CategoryDisjunctive h, HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalDiagrammatic h DiagramFree t n m Source #
Instance details Defined in OAlg.Entity.Slice.Free
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => NaturalTransformable h (->) (SDualBi (DiagramG DiagramFree t n m)) (SDualBi (DiagramG Diagram t n m)) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramG DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: h x y -> SDualBi (DiagramG DiagramFree t n m) x -> SDualBi (DiagramG DiagramFree t n m) y Source #
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: h x y -> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y Source #
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramG DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (DiagramFree t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
(ShowPoint a, Show a) => Show (DiagramFree t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> DiagramFree t n m a -> ShowS # show :: DiagramFree t n m a -> String # showList :: [DiagramFree t n m a] -> ShowS #
(EqPoint a, Eq a) => Eq (DiagramFree t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods (==) :: DiagramFree t n m a -> DiagramFree t n m a -> Bool # (/=) :: DiagramFree t n m a -> DiagramFree t n m a -> Bool #
Oriented a => Validable (DiagramFree t n m a) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: DiagramFree t n m a -> Statement Source #
type Dual1 (DiagramFree t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Free type Dual1 (DiagramFree t n m :: Type -> Type) = DiagramFree (Dual t) n m

dgfDiagram :: forall (t :: DiagramType) (n :: N') (m :: N') a. DiagramFree t n m a -> Diagram t n m a Source #

the underlying diagram.

dgfMapS :: forall h (t :: DiagramType) x y (n :: N') (m :: N'). (HomOrientedSlicedFree h, t ~ Dual (Dual t)) => h x y -> SDualBi (DiagramFree t n m) x -> SDualBi (DiagramFree t n m) y Source #

mapping of DiagramFree.

dgfMapCov :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Covariant h x y -> DiagramFree t n m x -> DiagramFree t n m y Source #

covariant mapping of DiagramFree.

dgfMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Contravariant h x y -> DiagramFree t n m x -> DiagramFree (Dual t) n m y Source #

contravariant mapping of DiagramFree.

Some Free Slice Diagram

data SomeFreeSliceDiagram (t :: DiagramType) (n :: N') (m :: N') x where Source #

some free slice diagram for kernels and cokernels diagrams.

Constructors

SomeFreeSliceKernel :: forall (k :: N') x. (Attestable k, Sliced (Free k) x) => Slice 'From (Free k) x -> SomeFreeSliceDiagram ('Parallel 'LeftToRight) ('S N1) ('S N0) x
SomeFreeSliceCokernel :: forall (k :: N') x. (Attestable k, Sliced (Free k) x) => Slice 'To (Free k) x -> SomeFreeSliceDiagram ('Parallel 'RightToLeft) ('S N1) ('S N0) x

Instances

Instances details

Diagrammatic SomeFreeSliceDiagram Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods diagram :: forall (t :: DiagramType) (n :: N') (m :: N') x. SomeFreeSliceDiagram t n m x -> Diagram t n m x Source #
(HomOrientedSlicedFree h, t ~ Dual (Dual t)) => ApplicativeG (SDualBi (SomeFreeSliceDiagram t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: h x y -> SDualBi (SomeFreeSliceDiagram t n m) x -> SDualBi (SomeFreeSliceDiagram t n m) y Source #
(HomOrientedSlicedFree h, FunctorialOriented h, t ~ Dual (Dual t)) => FunctorialG (SDualBi (SomeFreeSliceDiagram t n m)) h (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
type Dual1 (SomeFreeSliceDiagram t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Free type Dual1 (SomeFreeSliceDiagram t n m :: Type -> Type) = SomeFreeSliceDiagram (Dual t) n m

Duality

sfsdMapS :: forall h (t :: DiagramType) x y (n :: N') (m :: N'). (HomOrientedSlicedFree h, t ~ Dual (Dual t)) => h x y -> SDualBi (SomeFreeSliceDiagram t n m) x -> SDualBi (SomeFreeSliceDiagram t n m) y Source #

mapping of SomeFreeSliceDiagram.

sfsdMapCov :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Covariant h x y -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram t n m y Source #

covariant mapping of SomeFreeSliceDiagram.

sfsdMapCnt :: forall (h :: Type -> Type -> Type) x y (t :: DiagramType) (n :: N') (m :: N'). HomOrientedSlicedFree h => Variant2 'Contravariant h x y -> SomeFreeSliceDiagram t n m x -> SomeFreeSliceDiagram (Dual t) n m y Source #

contravariant mapping of SomeFreeSliceDiagram.

Cone Liftable

data ConeLiftable s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where Source #

predicate for a liftable conic object.

Property Let cl be in ConeLiftable s p d t n m x, then holds:

If cl matches ConeKernelLiftable c (LiftableFree l), then for any k in Any k holds: lftbBase (l k)' == kernelFactor c.
If cl matches ConeCokernelLiftable c (LiftableFree l), then for any k in Any k holds: lftbBase (l k)' == cokernelFactor c.

Constructors

ConeKernelLiftable :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x. KernelConic Cone d N1 x -> LiftableFree 'Projective x -> ConeLiftable Dst 'Projective d ('Parallel 'LeftToRight) ('S N1) ('S N0) x
ConeCokernelLiftable :: forall (d :: DiagramType -> N' -> N' -> Type -> Type) x. CokernelConic Cone d N1 x -> LiftableFree 'Injective x -> ConeLiftable Dst 'Injective d ('Parallel 'RightToLeft) ('S N1) ('S N0) x

Instances

Instances details

Conic ConeLiftable Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods cone :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. ConeLiftable s p d t n m x -> Cone s p d t n m x Source #
(NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => ApplicativeG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree s) x y -> SDualBi (ConeLiftable s p d t n m) x -> SDualBi (ConeLiftable s p d t n m) y Source #
(NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => FunctorialG (SDualBi (ConeLiftable s p d t n m)) (Inv2 (HomFree s)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
Show (d t n m x) => Show (ConeLiftable s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> ConeLiftable s p d t n m x -> ShowS # show :: ConeLiftable s p d t n m x -> String # showList :: [ConeLiftable s p d t n m x] -> ShowS #
(Show (d ('Parallel 'LeftToRight) n m x), Show (d ('Parallel 'LeftToRight) n m (Op x)), Validable (d ('Parallel 'LeftToRight) n m x), Validable (d ('Parallel 'LeftToRight) n m (Op x)), Distributive x, SlicedFree x, XStandardOrtOrientation x, NaturalDiagrammaticFree s d n m, n ~ N2, m ~ N1) => Validable (ConeLiftable s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: ConeLiftable s p d t n m x -> Statement Source #
type Dual1 (ConeLiftable s p d t n m :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Free type Dual1 (ConeLiftable s p d t n m :: Type -> Type) = ConeLiftable s (Dual p) d (Dual t) n m

cnLiftable :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. ConeLiftable s p d t n m x -> LiftableFree p x Source #

the underlying liftable.

cnlMapS :: forall s (d :: DiagramType -> N' -> N' -> Type -> Type) (p :: Perspective) (t :: DiagramType) x y (n :: N') (m :: N'). (NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) N2 N1, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) N2 N1, p ~ Dual (Dual p), t ~ Dual (Dual t)) => Inv2 (HomFree s) x y -> SDualBi (ConeLiftable s p d t n m) x -> SDualBi (ConeLiftable s p d t n m) y Source #

mapping of ConeLiftable.

Liftable Free

data LiftableFree (p :: Perspective) x where Source #

liftable according to a free slice.

Constructors

LiftableFree :: forall (p :: Perspective) x. (forall (k :: N'). Any k -> Liftable p (Free k) x) -> LiftableFree p x

Instances

Instances details

p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree Dst) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #
p ~ Dual (Dual p) => ApplicativeG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods amapG :: Inv2 (HomFree Mlt) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #
p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Dst)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
p ~ Dual (Dual p) => FunctorialG (SDualBi (LiftableFree p)) (Inv2 (HomFree Mlt)) (->) Source #
Instance details Defined in OAlg.Entity.Slice.Free
type Dual1 (LiftableFree p :: Type -> Type) Source #
Instance details Defined in OAlg.Entity.Slice.Free type Dual1 (LiftableFree p :: Type -> Type) = LiftableFree (Dual p)

liftFree :: forall (p :: Perspective) x (k :: N'). LiftableFree p x -> Any k -> Liftable p (Free k) x Source #

lifting a free slice.

type HomFree s = Sub (s, SldFr) (HomDisjEmpty s Op) Source #

homomorphism between free sliced structures.

lftFrMapSMlt :: forall (p :: Perspective) x y. p ~ Dual (Dual p) => Inv2 (HomFree Mlt) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #

mapping of LiftableFree.

lftFrMapSDst :: forall (p :: Perspective) x y. p ~ Dual (Dual p) => Inv2 (HomFree Dst) x y -> SDualBi (LiftableFree p) x -> SDualBi (LiftableFree p) y Source #

mapping of LiftableFree.

class (NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'LeftToRight) n m, NaturalDiagrammatic (Inv2 (HomFree s)) d ('Parallel 'RightToLeft) n m) => NaturalDiagrammaticFree s (d :: DiagramType -> N' -> N' -> Type -> Type) (n :: N') (m :: N') Source #

helper class to avoid undecidable instances.

Instances

Instances details

NaturalDiagrammaticFree Dst Diagram n m Source #
Instance details Defined in OAlg.Entity.Slice.Free
NaturalDiagrammaticFree Dst DiagramFree n m Source #
Instance details Defined in OAlg.Entity.Slice.Free
Attestable k => NaturalDiagrammaticFree Dst (SliceDiagram (Free k)) N2 N1 Source #
Instance details Defined in OAlg.Entity.Slice.Adjunction

type CokernelsLiftableSomeFree = CokernelsG ConeLiftable SomeFreeSliceDiagram N1 Source #

liftable cokernels for some free slice diagram

type CokernelLiftableSomeFree = CokernelG ConeLiftable SomeFreeSliceDiagram N1 Source #

liftable cokernels for some free slice diagram

Free Tip

data ConicFreeTip (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x where Source #

predicate for a Conic object with a free tip.

Property Let c be in ConicFreeTip c s p d t n m x, then holds:

slicePoint k == tip (cone c).

Constructors

ConicFreeTip :: forall (k :: N') x (c :: Type -> Perspective -> (DiagramType -> N' -> N' -> Type -> Type) -> DiagramType -> N' -> N' -> Type -> Type) s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N'). (Attestable k, Sliced (Free k) x) => Free k x -> c s p d t n m x -> ConicFreeTip c s p d t n m x

Instances

Instances details

Conic c => Conic (ConicFreeTip c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods cone :: forall s (p :: Perspective) (d :: DiagramType -> N' -> N' -> Type -> Type) (t :: DiagramType) (n :: N') (m :: N') x. ConicFreeTip c s p d t n m x -> Cone s p d t n m x Source #
Show (c s p d t n m x) => Show (ConicFreeTip c s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> ConicFreeTip c s p d t n m x -> ShowS # show :: ConicFreeTip c s p d t n m x -> String # showList :: [ConicFreeTip c s p d t n m x] -> ShowS #
(Conic c, Show (c s p d t n m x), Validable (c s p d t n m x)) => Validable (ConicFreeTip c s p d t n m x) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: ConicFreeTip c s p d t n m x -> Statement Source #

type KernelsSomeFreeFreeTip = KernelsG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 Source #

kernels with a free tip.

type KernelSomeFreeFreeTip = KernelG (ConicFreeTip Cone) SomeFreeSliceDiagram N1 Source #

kernel with a free tip.

data KernelSliceFromSomeFreeTip (n :: N') (i :: Type -> Type) c where Source #

predicate for a kernel with a start point of its diagram given by the slice index and a free universal tip.

Property Let KernelSliceFromSomeFreeTip k' i ker be in KernelSliceFromSomeFreeTip n c, then holds:

slicePoint i == s where DiagramParallelLR s _ _ = diagram ker.
slicePoint k' == tip (universalCone ker).

Constructors

KernelSliceFromSomeFreeTip :: forall (k' :: N') c (i :: Type -> Type) (n :: N'). (Attestable k', Sliced (Free k') c) => Free k' c -> i c -> Kernel n c -> KernelSliceFromSomeFreeTip n i c

Instances

Instances details

(Oriented c, Sliced i c) => Show (KernelSliceFromSomeFreeTip n i c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods showsPrec :: Int -> KernelSliceFromSomeFreeTip n i c -> ShowS # show :: KernelSliceFromSomeFreeTip n i c -> String # showList :: [KernelSliceFromSomeFreeTip n i c] -> ShowS #
(Distributive c, Sliced i c, XStandardEligibleConeKernel n c, XStandardEligibleConeFactorKernel n c, Typeable n) => Validable (KernelSliceFromSomeFreeTip n i c) Source #
Instance details Defined in OAlg.Entity.Slice.Free Methods valid :: KernelSliceFromSomeFreeTip n i c -> Statement Source #

Duality

toDualOpFreeDst :: (Distributive x, SlicedFree x) => Variant2 'Contravariant (Inv2 (HomFree Dst)) x (Op x) Source #

to dual operator.