Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type family Rel :: i -> j
- type family Reflected :: j -> i
- type family Coreflected :: j -> i
- class f ~| u | f k -> u, u j -> f where
- class Functor m => RelMonad m where
- class (rel ~ Rel, Tensor (RelCompose :: (j -> c) -> (j -> c) -> j -> c)) => RelComposed rel where
- type RelCompose :: (j -> c) -> (j -> c) -> j -> c
- rcomposed :: Functor f' => Iso (RelCompose f) (RelCompose f') (Compose (Lan rel f)) (Compose (Lan rel f'))
- newtype ComposeConst1 f g a b = ComposeConst1 {
- decomposeConst1 :: Compose2 (Lan2 Const1 f) g a b
Documentation
type family Rel :: i -> j Source
Rel should be a faithful functor that is also injective on objects.
and it sometimes has adjoints, if either exist, then they should satisfy the following relationship
Reflected
-|
Rel
-|
Coreflected
This provides the inclusion functor for a subcategory with objects indexed in i
into a category with objects in j
type Rel * * = Id0 | |
type Rel Constraint * = Dict | |
type Rel Constraint Constraint = IdC | |
type Rel Void * = No | |
type Rel * (k -> *) = Const1 k | |
type Rel Constraint (k -> Constraint) = ConstC k | |
type Rel (k -> *) (k -> *) = Id1 k | |
type Rel (k -> *) (k1 -> k -> *) = Const2 k k1 |
type family Reflected :: j -> i Source
The "reflector" of a
reflective sub-category with objects in j
of a category with objects in i
.
Reflected
-|
Rel
type family Coreflected :: j -> i Source
This "coreflector" of a coreflective sub-category with objects in j
of a category with objects in i
.
Rel
-|
Coreflected
type Coreflected * * = Id0 | |
type Coreflected Constraint Constraint = IdC | |
type Coreflected (k -> Constraint) Constraint = LimC k | |
type Coreflected (k -> *) * = Lim1 k | |
type Coreflected (k -> *) (k -> *) = Id1 k | |
type Coreflected (k -> k1 -> *) (k1 -> *) = Lim2 k k1 |
class f ~| u | f k -> u, u j -> f where Source
Relative adjoints
radj :: Iso (f a ~> b) (f a' ~> b') (Rel a ~> u b) (Rel a' ~> u b') Source
When Rel = Identity, a relative adjunction is just a normal adjunction, and you can use:
radj = adj.pre _Id
(~|) * * * Id0 Id0 | |
(~|) Constraint Constraint Constraint IdC IdC | |
(~|) * (i -> *) (i -> *) (Colim1 i) (Const1 i) | |
(~|) (k -> Constraint) Constraint Constraint (ConstC k) (LimC k) | |
(~|) (k -> *) * * (Const1 k) (Lim1 k) | |
(~|) (k -> *) (k -> *) (k -> *) (Id1 k) (Id1 k) | |
(~|) (k -> k -> *) (k -> *) (k -> *) (Const2 k k) (Lim2 k k) |
class Functor m => RelMonad m where Source
Relative monads
RelMonad Constraint Constraint IdC | |
RelMonad * (k -> *) (Const1 k) | |
RelMonad Constraint (k -> Constraint) (ConstC k) | |
RelMonad (k -> *) (k -> *) (Id1 k) | |
RelMonad (k -> *) (k -> k -> *) (Const2 k k) |
class (rel ~ Rel, Tensor (RelCompose :: (j -> c) -> (j -> c) -> j -> c)) => RelComposed rel where Source
type RelCompose :: (j -> c) -> (j -> c) -> j -> c Source
rcomposed :: Functor f' => Iso (RelCompose f) (RelCompose f') (Compose (Lan rel f)) (Compose (Lan rel f')) Source
RelComposed * * Id0 | |
RelComposed (k -> *) * (Const1 k) | |
RelComposed (k -> *) (k -> *) (Id1 k) |
newtype ComposeConst1 f g a b Source
ComposeConst1 | |
|
Functor * (k -> *) g => Functor * (k -> *) (ComposeConst1 k f g) | |
Tensor (* -> k -> *) (ComposeConst1 k) | |
Semitensor (* -> k -> *) (ComposeConst1 k) | |
Functor (* -> k -> *) ((* -> k -> *) -> * -> k -> *) (ComposeConst1 k) | |
Functor (* -> k -> *) (* -> k -> *) (ComposeConst1 k f) | |
type I (* -> k -> *) (ComposeConst1 k) = Const1 k | |
type Tensorable (* -> k -> *) (ComposeConst1 k) = Functor * (k -> *) |