| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Hask.Rel
- 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
Instances
| 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
Instances
| 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
Methods
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
Instances
| (~|) * * * 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
Instances
| 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
Associated Types
type RelCompose :: (j -> c) -> (j -> c) -> j -> c Source
Methods
rcomposed :: Functor f' => Iso (RelCompose f) (RelCompose f') (Compose (Lan rel f)) (Compose (Lan rel f')) Source
Instances
| RelComposed * * Id0 | |
| RelComposed (k -> *) * (Const1 k) | |
| RelComposed (k -> *) (k -> *) (Id1 k) |
newtype ComposeConst1 f g a b Source
Constructors
| ComposeConst1 | |
Fields
| |
Instances
| 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 -> *) |