Safe Haskell	Safe-Inferred
Language	Haskell2010

Hask.Iso

Contents

Synopsis

Iso

type Iso c d e s t a b = forall p. (Bifunctor p, Opd p ~ c, Dom2 p ~ d, Cod2 p ~ e) => p a b -> p s t Source

Get

data Get c r a b Source

Instances

(Category k c, Ob k c r, Ob k c a) => Functor k * (Get k c r a)
Category k c => Functor k (k -> k -> *) (Get k c)
(Category k c, Ob k c r) => Functor k (k -> *) (Get k c r)
type Dom k * (Get k c r a) = c
type Cod k * (Get k c r a) = (->)
type Dom k (k -> k -> *) (Get k c) = c
type Cod k (k -> k -> ) (Get k c) = Nat k (k -> ) (Op k c) (Nat k * c (->))
type Dom k (k -> *) (Get k c r) = Op k c
type Cod k (k -> ) (Get k c r) = Nat k c (->)

_Get :: Iso (->) (->) (->) (Get c r a b) (Get c r' a' b') (c a r) (c a' r') Source

get :: (Category c, Ob c a) => (Get c a a a -> Get c a s s) -> c s a Source

data Beget c r a b Source

Instances

(Category k c, Ob k c r, Ob k c a) => Functor k * (Beget k c r a)
Category k c => Functor k (k -> k -> *) (Beget k c)
(Category k c, Ob k c r) => Functor k (k -> *) (Beget k c r)
type Dom k * (Beget k c r a) = c
type Cod k * (Beget k c r a) = (->)
type Dom k (k -> k -> *) (Beget k c) = Op k c
type Cod k (k -> k -> ) (Beget k c) = Nat k (k -> ) (Op k c) (Nat k * c (->))
type Dom k (k -> *) (Beget k c r) = Op k c
type Cod k (k -> ) (Beget k c r) = Nat k c (->)

_Beget :: Iso (->) (->) (->) (Beget c r a b) (Beget c r' a' b') (c r b) (c r' b') Source

beget :: (Category c, Ob c b) => (Beget c b b b -> Beget c b t t) -> c b t Source

(#) :: (Beget (->) b b b -> Beget (->) b t t) -> b -> t Source

yoneda :: forall p f g a b. (Ob p a, FunctorOf p (->) g, FunctorOf p (->) (p b)) => Iso (->) (->) (->) (Nat p (->) (p a) f) (Nat p (->) (p b) g) (f a) (g b) Source