Pandora.Paradigm.Schemes.TUT

Documentation

newtype TUT ct ct' cu t t' u a

Constructors

TUT ((t :. (u :. t')) := a)

Instances

(Covariant t, Covariant t', Covariant u) => Covariant ((t <:<.>:> t') := u)

Defined in Pandora.Paradigm.Schemes.TUT

Methods

(<$>) :: (a -> b) -> ((t <:<.>:> t') := u) a -> ((t <:<.>:> t') := u) b

comap :: (a -> b) -> ((t <:<.>:> t') := u) a -> ((t <:<.>:> t') := u) b

(<$) :: a -> ((t <:<.>:> t') := u) b -> ((t <:<.>:> t') := u) a

($>) :: ((t <:<.>:> t') := u) a -> b -> ((t <:<.>:> t') := u) b

void :: ((t <:<.>:> t') := u) a -> ((t <:<.>:> t') := u) ()

loeb :: ((t <:<.>:> t') := u) (a <:= ((t <:<.>:> t') := u)) -> ((t <:<.>:> t') := u) a

(<&>) :: ((t <:<.>:> t') := u) a -> (a -> b) -> ((t <:<.>:> t') := u) b

(<$$>) :: Covariant u0 => (a -> b) -> ((((t <:<.>:> t') := u) :. u0) := a) -> (((t <:<.>:> t') := u) :. u0) := b

(<$$$>) :: (Covariant u0, Covariant v) => (a -> b) -> ((((t <:<.>:> t') := u) :. (u0 :. v)) := a) -> (((t <:<.>:> t') := u) :. (u0 :. v)) := b

(<$$$$>) :: (Covariant u0, Covariant v, Covariant w) => (a -> b) -> ((((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := a) -> (((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := b

(<&&>) :: Covariant u0 => ((((t <:<.>:> t') := u) :. u0) := a) -> (a -> b) -> (((t <:<.>:> t') := u) :. u0) := b

(<&&&>) :: (Covariant u0, Covariant v) => ((((t <:<.>:> t') := u) :. (u0 :. v)) := a) -> (a -> b) -> (((t <:<.>:> t') := u) :. (u0 :. v)) := b

(<&&&&>) :: (Covariant u0, Covariant v, Covariant w) => ((((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := a) -> (a -> b) -> (((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := b

(.#..) :: (((t <:<.>:> t') := u) ~ v a, Category v) => v c d -> ((v a :. v b) := c) -> (v a :. v b) := d

(.#...) :: (((t <:<.>:> t') := u) ~ v a, ((t <:<.>:> t') := u) ~ v b, Category v, Covariant (v a), Covariant (v b)) => v d e -> ((v a :. (v b :. v c)) := d) -> (v a :. (v b :. v c)) := e

(.#....) :: (((t <:<.>:> t') := u) ~ v a, ((t <:<.>:> t') := u) ~ v b, ((t <:<.>:> t') := u) ~ v c, Category v, Covariant (v a), Covariant (v b), Covariant (v c)) => v e f -> ((v a :. (v b :. (v c :. v d))) := e) -> (v a :. (v b :. (v c :. v d))) := f

(<$$) :: Covariant u0 => b -> ((((t <:<.>:> t') := u) :. u0) := a) -> (((t <:<.>:> t') := u) :. u0) := b

(<$$$) :: (Covariant u0, Covariant v) => b -> ((((t <:<.>:> t') := u) :. (u0 :. v)) := a) -> (((t <:<.>:> t') := u) :. (u0 :. v)) := b

(<$$$$) :: (Covariant u0, Covariant v, Covariant w) => b -> ((((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := a) -> (((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := b

($$>) :: Covariant u0 => ((((t <:<.>:> t') := u) :. u0) := a) -> b -> (((t <:<.>:> t') := u) :. u0) := b

($$$>) :: (Covariant u0, Covariant v) => ((((t <:<.>:> t') := u) :. (u0 :. v)) := a) -> b -> (((t <:<.>:> t') := u) :. (u0 :. v)) := b

($$$$>) :: (Covariant u0, Covariant v, Covariant w) => ((((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := a) -> b -> (((t <:<.>:> t') := u) :. (u0 :. (v :. w))) := b

(Covariant t', Covariant t, Adjoint t' t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Extendable u ((->) :: Type -> Type -> Type)) => Extendable ((t' <:<.>:> t) := u) ((->) :: Type -> Type -> Type)

Defined in Pandora.Paradigm.Schemes.TUT

Methods

(<<=) :: (((t' <:<.>:> t) := u) a -> b) -> ((t' <:<.>:> t) := u) a -> ((t' <:<.>:> t) := u) b

(Covariant_ t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Covariant_ t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Adjoint t t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Extractable u ((->) :: Type -> Type -> Type)) => Extractable ((t <:<.>:> t') := u) ((->) :: Type -> Type -> Type)

Defined in Pandora.Paradigm.Schemes.TUT

Methods

extract :: ((t <:<.>:> t') := u) a -> a

(Covariant_ t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Covariant_ t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Pointable u ((->) :: Type -> Type -> Type), Adjoint t' t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)) => Pointable ((t <:<.>:> t') := u) ((->) :: Type -> Type -> Type)

Defined in Pandora.Paradigm.Schemes.TUT

Methods

point :: a -> ((t <:<.>:> t') := u) a

(Covariant_ t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Covariant_ t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Covariant_ u ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)) => Covariant_ ((t <:<.>:> t') := u) ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)

Defined in Pandora.Paradigm.Schemes.TUT

Methods

(-<$>-) :: (a -> b) -> ((t <:<.>:> t') := u) a -> ((t <:<.>:> t') := u) b

(forall (u :: Type -> Type). Covariant u, Adjoint t' t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Distributive t ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)) => Liftable (t <:<.>:> t')

Defined in Pandora.Paradigm.Schemes.TUT

Methods

lift :: forall (u :: Type -> Type). Covariant_ u (->) (->) => u ~> (t <:<.>:> t') u

(forall (u :: Type -> Type). Covariant u, Adjoint t t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Distributive t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)) => Lowerable (t <:<.>:> t')

Defined in Pandora.Paradigm.Schemes.TUT

Methods

lower :: forall (u :: Type -> Type). Covariant_ u (->) (->) => (t <:<.>:> t') u ~> u

(Covariant ((t <:<.>:> u) t'), Covariant ((v <:<.>:> w) v'), Adjoint t w ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Adjoint t' v' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Adjoint t v ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Adjoint u v ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type), Adjoint v' t' ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)) => Adjoint ((t <:<.>:> u) t') ((v <:<.>:> w) v') ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type)

Defined in Pandora.Paradigm.Schemes

Methods

(-|) :: ((t <:<.>:> u) t' a -> b) -> a -> (v <:<.>:> w) v' b

(|-) :: (a -> (v <:<.>:> w) v' b) -> (t <:<.>:> u) t' a -> b

Interpreted (TUT ct ct' cu t t' u)

Defined in Pandora.Paradigm.Schemes.TUT

Associated Types

type Primary (TUT ct ct' cu t t' u) a

Methods

run :: TUT ct ct' cu t t' u a -> Primary (TUT ct ct' cu t t' u) a

unite :: Primary (TUT ct ct' cu t t' u) a -> TUT ct ct' cu t t' u a

(||=) :: Interpreted u0 => (Primary (TUT ct ct' cu t t' u) a -> Primary u0 b) -> TUT ct ct' cu t t' u a -> u0 b

(=||) :: Interpreted u0 => (TUT ct ct' cu t t' u a -> u0 b) -> Primary (TUT ct ct' cu t t' u) a -> Primary u0 b

(<$||=) :: (Covariant j, Interpreted u0) => (Primary (TUT ct ct' cu t t' u) a -> Primary u0 b) -> (j := TUT ct ct' cu t t' u a) -> j := u0 b

(<$$||=) :: (Covariant j, Covariant k, Interpreted u0) => (Primary (TUT ct ct' cu t t' u) a -> Primary u0 b) -> ((j :. k) := TUT ct ct' cu t t' u a) -> (j :. k) := u0 b

(<$$$||=) :: (Covariant j, Covariant k, Covariant l, Interpreted u0) => (Primary (TUT ct ct' cu t t' u) a -> Primary u0 b) -> ((j :. (k :. l)) := TUT ct ct' cu t t' u a) -> (j :. (k :. l)) := u0 b

(<$$$$||=) :: (Covariant j, Covariant k, Covariant l, Covariant m, Interpreted u0) => (Primary (TUT ct ct' cu t t' u) a -> Primary u0 b) -> ((j :. (k :. (l :. m))) := TUT ct ct' cu t t' u a) -> (j :. (k :. (l :. m))) := u0 b

(=||$>) :: (Covariant j, Interpreted u0) => (TUT ct ct' cu t t' u a -> u0 b) -> (j := Primary (TUT ct ct' cu t t' u) a) -> j := Primary u0 b

(=||$$>) :: (Covariant j, Covariant k, Interpreted u0) => (TUT ct ct' cu t t' u a -> u0 b) -> ((j :. k) := Primary (TUT ct ct' cu t t' u) a) -> (j :. k) := Primary u0 b

(=||$$$>) :: (Covariant j, Covariant k, Covariant l, Interpreted u0) => (TUT ct ct' cu t t' u a -> u0 b) -> ((j :. (k :. l)) := Primary (TUT ct ct' cu t t' u) a) -> (j :. (k :. l)) := Primary u0 b

(=||$$$$>) :: (Covariant j, Covariant k, Covariant l, Covariant m, Interpreted u0) => (TUT ct ct' cu t t' u a -> u0 b) -> ((j :. (k :. (l :. m))) := Primary (TUT ct ct' cu t t' u) a) -> (j :. (k :. (l :. m))) := Primary u0 b

type Primary (TUT ct ct' cu t t' u) a

Defined in Pandora.Paradigm.Schemes.TUT

type Primary (TUT ct ct' cu t t' u) a = (t :. (u :. t')) := a

type (<:<.>:>) = TUT Covariant Covariant Covariant infix 3

type (>:<.>:>) = TUT Contravariant Covariant Covariant infix 3

type (<:<.>:<) = TUT Covariant Covariant Contravariant infix 3

type (>:<.>:<) = TUT Contravariant Covariant Contravariant infix 3

type (<:>.<:>) = TUT Covariant Contravariant Covariant infix 3

type (>:>.<:>) = TUT Contravariant Contravariant Covariant infix 3

type (<:>.<:<) = TUT Covariant Contravariant Contravariant infix 3

type (>:>.<:<) = TUT Contravariant Contravariant Contravariant infix 3