Pandora.Paradigm.Primary.Transformer.Kan

Documentation

data family Kan (v :: * -> k) (t :: * -> *) (u :: * -> *) b a

Instances

Covariant ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) (Kan ('Right :: Type -> Wye Type) t u b)

Defined in Pandora.Paradigm.Primary.Transformer.Kan

Methods

(<$>) :: (a -> b0) -> Kan 'Right t u b a -> Kan 'Right t u b b0

Contravariant ((->) :: Type -> Type -> Type) ((->) :: Type -> Type -> Type) (Kan ('Left :: Type -> Wye Type) t u b)

Defined in Pandora.Paradigm.Primary.Transformer.Kan

Methods

(>$<) :: (a -> b0) -> Kan 'Left t u b b0 -> Kan 'Left t u b a

Interpreted ((->) :: Type -> Type -> Type) (Kan ('Left :: Type -> Wye Type) t u b)

Defined in Pandora.Paradigm.Primary.Transformer.Kan

Associated Types

type Primary (Kan 'Left t u b) a

Methods

run :: Kan 'Left t u b a -> Primary (Kan 'Left t u b) a

unite :: Primary (Kan 'Left t u b) a -> Kan 'Left t u b a

(||=) :: (Semigroupoid (->), Interpreted (->) u0) => (Primary (Kan 'Left t u b) a -> Primary u0 b0) -> Kan 'Left t u b a -> u0 b0

(=||) :: (Semigroupoid (->), Interpreted (->) u0) => (Kan 'Left t u b a -> u0 b0) -> Primary (Kan 'Left t u b) a -> Primary u0 b0

(<$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Interpreted (->) u0) => (Primary (Kan 'Left t u b) a -> Primary u0 b0) -> (j := Kan 'Left t u b a) -> (j := u0 b0)

(<$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Interpreted (->) u0) => (Primary (Kan 'Left t u b) a -> Primary u0 b0) -> ((j :. k) := Kan 'Left t u b a) -> ((j :. k) := u0 b0)

(<$$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted (->) u0) => (Primary (Kan 'Left t u b) a -> Primary u0 b0) -> ((j :. (k :. l)) := Kan 'Left t u b a) -> ((j :. (k :. l)) := u0 b0)

(<$$$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) n, Interpreted (->) u0) => (Primary (Kan 'Left t u b) a -> Primary u0 b0) -> ((j :. (k :. (l :. n))) := Kan 'Left t u b a) -> ((j :. (k :. (l :. n))) := u0 b0)

(=||$>) :: (Covariant (->) (->) j, Interpreted (->) u0) => (Kan 'Left t u b a -> u0 b0) -> (j := Primary (Kan 'Left t u b) a) -> (j := Primary u0 b0)

(=||$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted (->) u0) => (Kan 'Left t u b a -> u0 b0) -> ((j :. k) := Primary (Kan 'Left t u b) a) -> ((j :. k) := Primary u0 b0)

(=||$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted (->) u0) => (Kan 'Left t u b a -> u0 b0) -> ((j :. (k :. l)) := Primary (Kan 'Left t u b) a) -> ((j :. (k :. l)) := Primary u0 b0)

(=||$$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) n, Interpreted (->) u0) => (Kan 'Left t u b a -> u0 b0) -> ((j :. (k :. (l :. n))) := Primary (Kan 'Left t u b) a) -> ((j :. (k :. (l :. n))) := Primary u0 b0)

Interpreted ((->) :: Type -> Type -> Type) (Kan ('Right :: Type -> Wye Type) t u b)

Defined in Pandora.Paradigm.Primary.Transformer.Kan

Associated Types

type Primary (Kan 'Right t u b) a

Methods

run :: Kan 'Right t u b a -> Primary (Kan 'Right t u b) a

unite :: Primary (Kan 'Right t u b) a -> Kan 'Right t u b a

(||=) :: (Semigroupoid (->), Interpreted (->) u0) => (Primary (Kan 'Right t u b) a -> Primary u0 b0) -> Kan 'Right t u b a -> u0 b0

(=||) :: (Semigroupoid (->), Interpreted (->) u0) => (Kan 'Right t u b a -> u0 b0) -> Primary (Kan 'Right t u b) a -> Primary u0 b0

(<$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Interpreted (->) u0) => (Primary (Kan 'Right t u b) a -> Primary u0 b0) -> (j := Kan 'Right t u b a) -> (j := u0 b0)

(<$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Interpreted (->) u0) => (Primary (Kan 'Right t u b) a -> Primary u0 b0) -> ((j :. k) := Kan 'Right t u b a) -> ((j :. k) := u0 b0)

(<$$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted (->) u0) => (Primary (Kan 'Right t u b) a -> Primary u0 b0) -> ((j :. (k :. l)) := Kan 'Right t u b a) -> ((j :. (k :. l)) := u0 b0)

(<$$$$||=) :: (Semigroupoid (->), Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) n, Interpreted (->) u0) => (Primary (Kan 'Right t u b) a -> Primary u0 b0) -> ((j :. (k :. (l :. n))) := Kan 'Right t u b a) -> ((j :. (k :. (l :. n))) := u0 b0)

(=||$>) :: (Covariant (->) (->) j, Interpreted (->) u0) => (Kan 'Right t u b a -> u0 b0) -> (j := Primary (Kan 'Right t u b) a) -> (j := Primary u0 b0)

(=||$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Interpreted (->) u0) => (Kan 'Right t u b a -> u0 b0) -> ((j :. k) := Primary (Kan 'Right t u b) a) -> ((j :. k) := Primary u0 b0)

(=||$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Interpreted (->) u0) => (Kan 'Right t u b a -> u0 b0) -> ((j :. (k :. l)) := Primary (Kan 'Right t u b) a) -> ((j :. (k :. l)) := Primary u0 b0)

(=||$$$$>) :: (Covariant (->) (->) j, Covariant (->) (->) k, Covariant (->) (->) l, Covariant (->) (->) n, Interpreted (->) u0) => (Kan 'Right t u b a -> u0 b0) -> ((j :. (k :. (l :. n))) := Primary (Kan 'Right t u b) a) -> ((j :. (k :. (l :. n))) := Primary u0 b0)

data Kan ('Left :: Type -> Wye Type) t u b a

Defined in Pandora.Paradigm.Primary.Transformer.Kan

data Kan ('Left :: Type -> Wye Type) t u b a = Lan ((t b -> a) -> u b)

data Kan ('Right :: Type -> Wye Type) t u b a

Defined in Pandora.Paradigm.Primary.Transformer.Kan

data Kan ('Right :: Type -> Wye Type) t u b a = Ran ((a -> t b) -> u b)

type Primary (Kan ('Left :: Type -> Wye Type) t u b) a

Defined in Pandora.Paradigm.Primary.Transformer.Kan

type Primary (Kan ('Left :: Type -> Wye Type) t u b) a = (t b -> a) -> u b

type Primary (Kan ('Right :: Type -> Wye Type) t u b) a

Defined in Pandora.Paradigm.Primary.Transformer.Kan

type Primary (Kan ('Right :: Type -> Wye Type) t u b) a = (a -> t b) -> u b