data-category 0.6.1 → 0.6.2
raw patch · 11 files changed
+222/−233 lines, 11 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Data.Category: instance Category (->)
- Data.Category: instance Category k => Category (Op k)
- Data.Category: unOp :: Op k a b -> k b a
- Data.Category.Adjunction: AdjArrow :: Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
- Data.Category.Adjunction: counit :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
- Data.Category.Adjunction: instance Category AdjArrow
- Data.Category.Adjunction: leftAdjoint :: Adjunction c d f g -> f
- Data.Category.Adjunction: rightAdjoint :: Adjunction c d f g -> g
- Data.Category.Adjunction: unit :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
- Data.Category.Boolean: F2T :: Boolean Fls Tru
- Data.Category.Boolean: Fls :: Boolean Fls Fls
- Data.Category.Boolean: Tru :: Boolean Tru Tru
- Data.Category.Boolean: instance CartesianClosed Boolean
- Data.Category.Boolean: instance Category Boolean
- Data.Category.Boolean: instance HasBinaryCoproducts Boolean
- Data.Category.Boolean: instance HasBinaryProducts Boolean
- Data.Category.Boolean: instance HasInitialObject Boolean
- Data.Category.Boolean: instance HasTerminalObject Boolean
- Data.Category.CartesianClosed: Apply :: Apply
- Data.Category.CartesianClosed: Tuple :: Tuple
- Data.Category.CartesianClosed: data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *)
- Data.Category.CartesianClosed: data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *)
- Data.Category.CartesianClosed: instance (Category c1, Category c2) => Functor (Apply c1 c2)
- Data.Category.CartesianClosed: instance (Category c1, Category c2) => Functor (Tuple c1 c2)
- Data.Category.CartesianClosed: instance CartesianClosed (->)
- Data.Category.CartesianClosed: instance CartesianClosed Cat
- Data.Category.CartesianClosed: instance CartesianClosed k => Functor (ExpFunctor k)
- Data.Category.Comma: CommaA :: CommaO t s (a, b) -> Dom t a a' -> Dom s b b' -> CommaO t s (a', b') -> (t :/\: s) (a, b) (a', b')
- Data.Category.Comma: CommaO :: Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
- Data.Category.Comma: instance (Category (Dom t), Category (Dom s)) => Category (t :/\: s)
- Data.Category.Coproduct: I1 :: c1 a1 b1 -> :++: c1 c2 (I1 a1) (I1 b1)
- Data.Category.Coproduct: I12 :: Obj c1 a -> Obj c2 b -> :>>: c1 c2 (I1 a) (I2 b)
- Data.Category.Coproduct: I1A :: c1 a1 b1 -> :>>: c1 c2 (I1 a1) (I1 b1)
- Data.Category.Coproduct: I2 :: c2 a2 b2 -> :++: c1 c2 (I2 a2) (I2 b2)
- Data.Category.Coproduct: I2A :: c2 a2 b2 -> :>>: c1 c2 (I2 a2) (I2 b2)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Category (c1 :++: c2)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Category (c1 :>>: c2)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Functor (Cotuple1 c1 c2 a1)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Functor (Cotuple2 c1 c2 a2)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Functor (Inj1 c1 c2)
- Data.Category.Coproduct: instance (Category c1, Category c2) => Functor (Inj2 c1 c2)
- Data.Category.Coproduct: instance (Functor f, Functor g, Dom f ~ Dom g, Cod f ~ Cod g) => Functor (NatAsFunctor f g)
- Data.Category.Coproduct: instance (Functor f1, Functor f2) => Functor (f1 :+++: f2)
- Data.Category.Coproduct: instance Category k => Functor (CodiagCoprod k)
- Data.Category.Cube: Cons :: Sign0 -> ACube n -> ACube (S n)
- Data.Category.Cube: Nil :: ACube Z
- Data.Category.Cube: S :: Cube x y -> Cube (S x) (S y)
- Data.Category.Cube: X :: Cube x y -> Cube (S x) y
- Data.Category.Cube: Y :: Sign -> Cube x y -> Cube x (S y)
- Data.Category.Cube: Z :: Cube Z Z
- Data.Category.Cube: instance Category Cube
- Data.Category.Cube: instance Functor Add
- Data.Category.Cube: instance Functor Forget
- Data.Category.Cube: instance HasTerminalObject Cube
- Data.Category.Cube: instance TensorProduct Add
- Data.Category.Dialg: DialgA :: Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
- Data.Category.Dialg: Dialgebra :: Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a
- Data.Category.Dialg: instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (ForgetAlg m)
- Data.Category.Dialg: instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (FreeAlg m)
- Data.Category.Dialg: instance Category (Dialg f g)
- Data.Category.Dialg: instance HasInitialObject (Dialg (Tuple1 (->) (->) ()) (DiagProd (->)))
- Data.Category.Fix: instance CartesianClosed (f (Fix f)) => CartesianClosed (Fix f)
- Data.Category.Fix: instance Category (f (Fix f)) => Category (Fix f)
- Data.Category.Fix: instance Category (f (Fix f)) => Functor (Wrap f)
- Data.Category.Fix: instance HasBinaryCoproducts (f (Fix f)) => HasBinaryCoproducts (Fix f)
- Data.Category.Fix: instance HasBinaryProducts (f (Fix f)) => HasBinaryProducts (Fix f)
- Data.Category.Fix: instance HasInitialObject (f (Fix f)) => HasInitialObject (Fix f)
- Data.Category.Fix: instance HasTerminalObject (f (Fix f)) => HasTerminalObject (Fix f)
- Data.Category.Functor: (:.:) :: g -> h -> g :.: h
- Data.Category.Functor: CatA :: ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
- Data.Category.Functor: Const :: Obj c2 x -> Const c1 c2 x
- Data.Category.Functor: Opposite :: f -> Opposite f
- Data.Category.Functor: instance (Category (Cod g), Category (Dom h)) => Functor (g :.: h)
- Data.Category.Functor: instance (Category (Dom f), Category (Cod f)) => Functor (Opposite f)
- Data.Category.Functor: instance (Category c1, Category c2) => Functor (Const c1 c2 x)
- Data.Category.Functor: instance (Category c1, Category c2) => Functor (Proj1 c1 c2)
- Data.Category.Functor: instance (Category c1, Category c2) => Functor (Proj2 c1 c2)
- Data.Category.Functor: instance (Category c1, Category c2) => Functor (Tuple1 c1 c2 a1)
- Data.Category.Functor: instance (Functor f1, Functor f2) => Functor (f1 :***: f2)
- Data.Category.Functor: instance Category Cat
- Data.Category.Functor: instance Category k => Functor (DiagProd k)
- Data.Category.Functor: instance Category k => Functor (Hom k)
- Data.Category.Functor: instance Category k => Functor (Id k)
- Data.Category.Functor: instance Category k => Functor (OpOp k)
- Data.Category.Functor: instance Category k => Functor (OpOpInv k)
- Data.Category.Kleisli: Kleisli :: Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
- Data.Category.Kleisli: instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjF m)
- Data.Category.Kleisli: instance (Functor m, Dom m ~ k, Cod m ~ k) => Functor (KleisliAdjG m)
- Data.Category.Kleisli: instance Category (Kleisli m)
- Data.Category.Limit: (:*:) :: p -> q -> p :*: q
- Data.Category.Limit: (:+:) :: p -> q -> p :+: q
- Data.Category.Limit: Diag :: Diag j k
- Data.Category.Limit: instance (Category (Dom p), Category (Cod p)) => Functor (p :*: q)
- Data.Category.Limit: instance (Category (Dom p), Category (Cod p)) => Functor (p :+: q)
- Data.Category.Limit: instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d)
- Data.Category.Limit: instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d)
- Data.Category.Limit: instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d)
- Data.Category.Limit: instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d)
- Data.Category.Limit: instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2)
- Data.Category.Limit: instance (Category j, Category k) => Functor (Diag j k)
- Data.Category.Limit: instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2)
- Data.Category.Limit: instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :>>: c2)
- Data.Category.Limit: instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2)
- Data.Category.Limit: instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :>>: c2)
- Data.Category.Limit: instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k
- Data.Category.Limit: instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k
- Data.Category.Limit: instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2)
- Data.Category.Limit: instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2)
- Data.Category.Limit: instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k
- Data.Category.Limit: instance (HasTerminalObject (i :>>: j), Category k) => HasColimits (i :>>: j) k
- Data.Category.Limit: instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2)
- Data.Category.Limit: instance Category k => HasColimits Unit k
- Data.Category.Limit: instance Category k => HasLimits Unit k
- Data.Category.Limit: instance HasBinaryCoproducts Cat
- Data.Category.Limit: instance HasBinaryCoproducts Unit
- Data.Category.Limit: instance HasBinaryCoproducts k => Functor (CoproductFunctor k)
- Data.Category.Limit: instance HasBinaryCoproducts k => HasBinaryProducts (Op k)
- Data.Category.Limit: instance HasBinaryProducts (->)
- Data.Category.Limit: instance HasBinaryProducts Cat
- Data.Category.Limit: instance HasBinaryProducts Unit
- Data.Category.Limit: instance HasBinaryProducts k => Functor (ProductFunctor k)
- Data.Category.Limit: instance HasBinaryProducts k => HasBinaryCoproducts (Op k)
- Data.Category.Limit: instance HasColimits j k => Functor (ColimitFunctor j k)
- Data.Category.Limit: instance HasInitialObject (->)
- Data.Category.Limit: instance HasInitialObject Cat
- Data.Category.Limit: instance HasInitialObject Unit
- Data.Category.Limit: instance HasInitialObject k => HasColimits Void k
- Data.Category.Limit: instance HasInitialObject k => HasTerminalObject (Op k)
- Data.Category.Limit: instance HasLimits j k => Functor (LimitFunctor j k)
- Data.Category.Limit: instance HasTerminalObject (->)
- Data.Category.Limit: instance HasTerminalObject Cat
- Data.Category.Limit: instance HasTerminalObject Unit
- Data.Category.Limit: instance HasTerminalObject k => HasInitialObject (Op k)
- Data.Category.Limit: instance HasTerminalObject k => HasLimits Void k
- Data.Category.Monoidal: MonoidValue :: f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
- Data.Category.Monoidal: comultiply :: ComonoidObject f a -> forall k. Cod f ~ k => k a (f :% (a, a))
- Data.Category.Monoidal: counit :: ComonoidObject f a -> forall k. Cod f ~ k => k a (Unit f)
- Data.Category.Monoidal: instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k)
- Data.Category.Monoidal: instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k)
- Data.Category.Monoidal: instance Category (MonoidAsCategory f m)
- Data.Category.Monoidal: instance Category k => TensorProduct (EndoFunctorCompose k)
- Data.Category.Monoidal: multiply :: MonoidObject f a -> forall k. Cod f ~ k => k ((f :% (a, a))) a
- Data.Category.Monoidal: unit :: MonoidObject f a -> forall k. Cod f ~ k => k (Unit f) a
- Data.Category.NNO: instance (Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s)
- Data.Category.NNO: instance HasNaturalNumberObject (->)
- Data.Category.NNO: instance HasNaturalNumberObject Cat
- Data.Category.NaturalTransformation: Nat :: f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
- Data.Category.NaturalTransformation: instance (Category c, Category d) => Category (Nat c d)
- Data.Category.NaturalTransformation: instance (Category c, Category d, Category e) => Functor (FunctorCompose c d e)
- Data.Category.NaturalTransformation: instance (Functor f, Functor h) => Functor (Wrap f h)
- Data.Category.NaturalTransformation: unCom :: Com f g z -> Component f g z
- Data.Category.Presheaf: instance Category k => CartesianClosed (Presheaves k)
- Data.Category.Presheaf: pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
- Data.Category.Presheaf: type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k)
- Data.Category.Presheaf: type Presheaves k = Nat (Op k) (->)
- Data.Category.Product: (:**:) :: c1 a1 b1 -> c2 a2 b2 -> :**: c1 c2 (a1, a2) (b1, b2)
- Data.Category.Product: instance (Category c1, Category c2) => Category (c1 :**: c2)
- Data.Category.RepresentableFunctor: represent :: Representable f repObj -> forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
- Data.Category.RepresentableFunctor: representedFunctor :: Representable f repObj -> f
- Data.Category.RepresentableFunctor: representingObject :: Representable f repObj -> Obj (Dom f) repObj
- Data.Category.RepresentableFunctor: universalElement :: Representable f repObj -> forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
- Data.Category.Simplex: Fs :: Fin n -> Fin (S n)
- Data.Category.Simplex: Fz :: Fin (S n)
- Data.Category.Simplex: X :: Simplex x (S y) -> Simplex (S x) (S y)
- Data.Category.Simplex: Y :: Simplex x y -> Simplex x (S y)
- Data.Category.Simplex: Z :: Simplex Z Z
- Data.Category.Simplex: instance Category Simplex
- Data.Category.Simplex: instance Functor Add
- Data.Category.Simplex: instance Functor Forget
- Data.Category.Simplex: instance HasInitialObject Simplex
- Data.Category.Simplex: instance HasTerminalObject Simplex
- Data.Category.Simplex: instance TensorProduct Add
- Data.Category.Simplex: instance TensorProduct f => Functor (Replicate f a)
- Data.Category.Unit: Unit :: Unit () ()
- Data.Category.Unit: instance Category Unit
- Data.Category.Void: instance Category Void
- Data.Category.Void: instance Category k => Functor (Magic k)
- Data.Category.Yoneda: instance (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => Functor (Yoneda k f)
+ Data.Category: [unOp] :: Op k a b -> k b a
+ Data.Category: instance Data.Category.Category (->)
+ Data.Category: instance Data.Category.Category k => Data.Category.Category (Data.Category.Op k)
+ Data.Category.Adjunction: [AdjArrow] :: (Category c, Category d) => Adjunction c d f g -> AdjArrow (CatW c) (CatW d)
+ Data.Category.Adjunction: [counit] :: Adjunction c d f g -> Nat c c (f :.: g) (Id c)
+ Data.Category.Adjunction: [leftAdjoint] :: Adjunction c d f g -> f
+ Data.Category.Adjunction: [rightAdjoint] :: Adjunction c d f g -> g
+ Data.Category.Adjunction: [unit] :: Adjunction c d f g -> Nat d d (Id d) (g :.: f)
+ Data.Category.Adjunction: instance Data.Category.Category Data.Category.Adjunction.AdjArrow
+ Data.Category.Boolean: [F2T] :: Boolean Fls Tru
+ Data.Category.Boolean: [Fls] :: Boolean Fls Fls
+ Data.Category.Boolean: [Tru] :: Boolean Tru Tru
+ Data.Category.Boolean: instance Data.Category.CartesianClosed.CartesianClosed Data.Category.Boolean.Boolean
+ Data.Category.Boolean: instance Data.Category.Category Data.Category.Boolean.Boolean
+ Data.Category.Boolean: instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Boolean.Boolean
+ Data.Category.Boolean: instance Data.Category.Limit.HasBinaryProducts Data.Category.Boolean.Boolean
+ Data.Category.Boolean: instance Data.Category.Limit.HasInitialObject Data.Category.Boolean.Boolean
+ Data.Category.Boolean: instance Data.Category.Limit.HasTerminalObject Data.Category.Boolean.Boolean
+ Data.Category.CartesianClosed: instance Data.Category.CartesianClosed.CartesianClosed (->)
+ Data.Category.CartesianClosed: instance Data.Category.CartesianClosed.CartesianClosed Data.Category.Functor.Cat
+ Data.Category.CartesianClosed: instance Data.Category.CartesianClosed.CartesianClosed k => Data.Category.Functor.Functor (Data.Category.CartesianClosed.ExpFunctor k)
+ Data.Category.CartesianClosed: instance Data.Category.Category k => Data.Category.CartesianClosed.CartesianClosed (Data.Category.NaturalTransformation.Presheaves k)
+ Data.Category.CartesianClosed: pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z
+ Data.Category.CartesianClosed: type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite ((ProductFunctor (Presheaves k) :.: Tuple2 (Presheaves k) (Presheaves k) y) :.: YonedaEmbedding k)
+ Data.Category.CartesianClosed: type family Exponential k y z :: *;
+ Data.Category.CartesianClosed: }
+ Data.Category.Comma: [CommaA] :: CommaO t s (a, b) -> Dom t a a' -> Dom s b b' -> CommaO t s (a', b') -> (t :/\: s) (a, b) (a', b')
+ Data.Category.Comma: [CommaO] :: (Cod t ~ k, Cod s ~ k) => Obj (Dom t) a -> k (t :% a) (s :% b) -> Obj (Dom s) b -> CommaO t s (a, b)
+ Data.Category.Comma: instance (Data.Category.Category (Data.Category.Functor.Dom t), Data.Category.Category (Data.Category.Functor.Dom s)) => Data.Category.Category (t Data.Category.Comma.:/\: s)
+ Data.Category.Coproduct: [I12] :: Obj c1 a -> Obj c2 b -> (:>>:) c1 c2 (I1 a) (I2 b)
+ Data.Category.Coproduct: [I1A] :: c1 a1 b1 -> (:>>:) c1 c2 (I1 a1) (I1 b1)
+ Data.Category.Coproduct: [I1] :: c1 a1 b1 -> (:++:) c1 c2 (I1 a1) (I1 b1)
+ Data.Category.Coproduct: [I2A] :: c2 a2 b2 -> (:>>:) c1 c2 (I2 a2) (I2 b2)
+ Data.Category.Coproduct: [I2] :: c2 a2 b2 -> (:++:) c1 c2 (I2 a2) (I2 b2)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Category (c1 Data.Category.Coproduct.:++: c2)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Category (c1 Data.Category.Coproduct.:>>: c2)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Cotuple1 c1 c2 a1)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Cotuple2 c1 c2 a2)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Inj1 c1 c2)
+ Data.Category.Coproduct: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Coproduct.Inj2 c1 c2)
+ Data.Category.Coproduct: instance (Data.Category.Functor.Functor f, Data.Category.Functor.Functor g, Data.Category.Functor.Dom f ~ Data.Category.Functor.Dom g, Data.Category.Functor.Cod f ~ Data.Category.Functor.Cod g) => Data.Category.Functor.Functor (Data.Category.Coproduct.NatAsFunctor f g)
+ Data.Category.Coproduct: instance (Data.Category.Functor.Functor f1, Data.Category.Functor.Functor f2) => Data.Category.Functor.Functor (f1 Data.Category.Coproduct.:+++: f2)
+ Data.Category.Coproduct: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Coproduct.CodiagCoprod k)
+ Data.Category.Cube: [Cons] :: Sign0 -> ACube n -> ACube (S n)
+ Data.Category.Cube: [Nil] :: ACube Z
+ Data.Category.Cube: [S] :: Cube x y -> Cube (S x) (S y)
+ Data.Category.Cube: [X] :: Cube x y -> Cube (S x) y
+ Data.Category.Cube: [Y] :: Sign -> Cube x y -> Cube x (S y)
+ Data.Category.Cube: [Z] :: Cube Z Z
+ Data.Category.Cube: instance Data.Category.Category Data.Category.Cube.Cube
+ Data.Category.Cube: instance Data.Category.Functor.Functor Data.Category.Cube.Add
+ Data.Category.Cube: instance Data.Category.Functor.Functor Data.Category.Cube.Forget
+ Data.Category.Cube: instance Data.Category.Limit.HasTerminalObject Data.Category.Cube.Cube
+ Data.Category.Cube: instance Data.Category.Monoidal.TensorProduct Data.Category.Cube.Add
+ Data.Category.Dialg: [DialgA] :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => Dialgebra f g a -> Dialgebra f g b -> c a b -> Dialg f g a b
+ Data.Category.Dialg: [Dialgebra] :: (Category c, Category d, Dom f ~ c, Dom g ~ c, Cod f ~ d, Cod g ~ d, Functor f, Functor g) => Obj c a -> d (f :% a) (g :% a) -> Dialgebra f g a
+ Data.Category.Dialg: instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m ~ k, Data.Category.Functor.Cod m ~ k) => Data.Category.Functor.Functor (Data.Category.Dialg.ForgetAlg m)
+ Data.Category.Dialg: instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m ~ k, Data.Category.Functor.Cod m ~ k) => Data.Category.Functor.Functor (Data.Category.Dialg.FreeAlg m)
+ Data.Category.Dialg: instance Data.Category.Category (Data.Category.Dialg.Dialg f g)
+ Data.Category.Dialg: instance Data.Category.Limit.HasInitialObject (Data.Category.Dialg.Dialg (Data.Category.Functor.Tuple1 (->) (->) ()) (Data.Category.Functor.DiagProd (->)))
+ Data.Category.Fix: instance Data.Category.CartesianClosed.CartesianClosed (f (Data.Category.Fix.Fix f)) => Data.Category.CartesianClosed.CartesianClosed (Data.Category.Fix.Fix f)
+ Data.Category.Fix: instance Data.Category.Category (f (Data.Category.Fix.Fix f)) => Data.Category.Category (Data.Category.Fix.Fix f)
+ Data.Category.Fix: instance Data.Category.Category (f (Data.Category.Fix.Fix f)) => Data.Category.Functor.Functor (Data.Category.Fix.Wrap f)
+ Data.Category.Fix: instance Data.Category.Limit.HasBinaryCoproducts (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Fix.Fix f)
+ Data.Category.Fix: instance Data.Category.Limit.HasBinaryProducts (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasBinaryProducts (Data.Category.Fix.Fix f)
+ Data.Category.Fix: instance Data.Category.Limit.HasInitialObject (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasInitialObject (Data.Category.Fix.Fix f)
+ Data.Category.Fix: instance Data.Category.Limit.HasTerminalObject (f (Data.Category.Fix.Fix f)) => Data.Category.Limit.HasTerminalObject (Data.Category.Fix.Fix f)
+ Data.Category.Functor: [:.:] :: (Functor g, Functor h, Cod h ~ Dom g) => g -> h -> g :.: h
+ Data.Category.Functor: [CatA] :: (Functor ftag, Category (Dom ftag), Category (Cod ftag)) => ftag -> Cat (CatW (Dom ftag)) (CatW (Cod ftag))
+ Data.Category.Functor: [Const] :: Obj c2 x -> Const c1 c2 x
+ Data.Category.Functor: [Opposite] :: Functor f => f -> Opposite f
+ Data.Category.Functor: instance (Data.Category.Category (Data.Category.Functor.Cod g), Data.Category.Category (Data.Category.Functor.Dom h)) => Data.Category.Functor.Functor (g Data.Category.Functor.:.: h)
+ Data.Category.Functor: instance (Data.Category.Category (Data.Category.Functor.Dom f), Data.Category.Category (Data.Category.Functor.Cod f)) => Data.Category.Functor.Functor (Data.Category.Functor.Opposite f)
+ Data.Category.Functor: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Const c1 c2 x)
+ Data.Category.Functor: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Proj1 c1 c2)
+ Data.Category.Functor: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Proj2 c1 c2)
+ Data.Category.Functor: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.Functor.Tuple1 c1 c2 a1)
+ Data.Category.Functor: instance (Data.Category.Functor.Functor f1, Data.Category.Functor.Functor f2) => Data.Category.Functor.Functor (f1 Data.Category.Functor.:***: f2)
+ Data.Category.Functor: instance Data.Category.Category Data.Category.Functor.Cat
+ Data.Category.Functor: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.DiagProd k)
+ Data.Category.Functor: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.Hom k)
+ Data.Category.Functor: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.Id k)
+ Data.Category.Functor: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.OpOp k)
+ Data.Category.Functor: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Functor.OpOpInv k)
+ Data.Category.Functor: type family (:%) ftag a :: *;
+ Data.Category.Functor: }
+ Data.Category.Kleisli: [Kleisli] :: (Functor m, Dom m ~ k, Cod m ~ k) => Monad m -> Obj k b -> k a (m :% b) -> Kleisli m a b
+ Data.Category.Kleisli: instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m ~ k, Data.Category.Functor.Cod m ~ k) => Data.Category.Functor.Functor (Data.Category.Kleisli.KleisliAdjF m)
+ Data.Category.Kleisli: instance (Data.Category.Functor.Functor m, Data.Category.Functor.Dom m ~ k, Data.Category.Functor.Cod m ~ k) => Data.Category.Functor.Functor (Data.Category.Kleisli.KleisliAdjG m)
+ Data.Category.Kleisli: instance Data.Category.Category (Data.Category.Kleisli.Kleisli m)
+ Data.Category.Limit: [:*:] :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryProducts k) => p -> q -> p :*: q
+ Data.Category.Limit: [:+:] :: (Functor p, Functor q, Dom p ~ Dom q, Cod p ~ k, Cod q ~ k, HasBinaryCoproducts k) => p -> q -> p :+: q
+ Data.Category.Limit: [Diag] :: Diag j k
+ Data.Category.Limit: instance (Data.Category.Category (Data.Category.Functor.Dom p), Data.Category.Category (Data.Category.Functor.Cod p)) => Data.Category.Functor.Functor (p Data.Category.Limit.:*: q)
+ Data.Category.Limit: instance (Data.Category.Category (Data.Category.Functor.Dom p), Data.Category.Category (Data.Category.Functor.Cod p)) => Data.Category.Functor.Functor (p Data.Category.Limit.:+: q)
+ Data.Category.Limit: instance (Data.Category.Category c, Data.Category.Limit.HasBinaryCoproducts d) => Data.Category.Limit.HasBinaryCoproducts (Data.Category.NaturalTransformation.Nat c d)
+ Data.Category.Limit: instance (Data.Category.Category c, Data.Category.Limit.HasBinaryProducts d) => Data.Category.Limit.HasBinaryProducts (Data.Category.NaturalTransformation.Nat c d)
+ Data.Category.Limit: instance (Data.Category.Category c, Data.Category.Limit.HasInitialObject d) => Data.Category.Limit.HasInitialObject (Data.Category.NaturalTransformation.Nat c d)
+ Data.Category.Limit: instance (Data.Category.Category c, Data.Category.Limit.HasTerminalObject d) => Data.Category.Limit.HasTerminalObject (Data.Category.NaturalTransformation.Nat c d)
+ Data.Category.Limit: instance (Data.Category.Category c1, Data.Category.Limit.HasTerminalObject c2) => Data.Category.Limit.HasTerminalObject (c1 Data.Category.Coproduct.:>>: c2)
+ Data.Category.Limit: instance (Data.Category.Category j, Data.Category.Category k) => Data.Category.Functor.Functor (Data.Category.Limit.Diag j k)
+ Data.Category.Limit: instance (Data.Category.Limit.HasBinaryCoproducts c1, Data.Category.Limit.HasBinaryCoproducts c2) => Data.Category.Limit.HasBinaryCoproducts (c1 Data.Category.Coproduct.:>>: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasBinaryCoproducts c1, Data.Category.Limit.HasBinaryCoproducts c2) => Data.Category.Limit.HasBinaryCoproducts (c1 Data.Category.Product.:**: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasBinaryProducts c1, Data.Category.Limit.HasBinaryProducts c2) => Data.Category.Limit.HasBinaryProducts (c1 Data.Category.Coproduct.:>>: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasBinaryProducts c1, Data.Category.Limit.HasBinaryProducts c2) => Data.Category.Limit.HasBinaryProducts (c1 Data.Category.Product.:**: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasColimits i k, Data.Category.Limit.HasColimits j k, Data.Category.Limit.HasBinaryCoproducts k) => Data.Category.Limit.HasColimits (i Data.Category.Coproduct.:++: j) k
+ Data.Category.Limit: instance (Data.Category.Limit.HasInitialObject (i Data.Category.Coproduct.:>>: j), Data.Category.Category k) => Data.Category.Limit.HasLimits (i Data.Category.Coproduct.:>>: j) k
+ Data.Category.Limit: instance (Data.Category.Limit.HasInitialObject c1, Data.Category.Category c2) => Data.Category.Limit.HasInitialObject (c1 Data.Category.Coproduct.:>>: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasInitialObject c1, Data.Category.Limit.HasInitialObject c2) => Data.Category.Limit.HasInitialObject (c1 Data.Category.Product.:**: c2)
+ Data.Category.Limit: instance (Data.Category.Limit.HasLimits i k, Data.Category.Limit.HasLimits j k, Data.Category.Limit.HasBinaryProducts k) => Data.Category.Limit.HasLimits (i Data.Category.Coproduct.:++: j) k
+ Data.Category.Limit: instance (Data.Category.Limit.HasTerminalObject (i Data.Category.Coproduct.:>>: j), Data.Category.Category k) => Data.Category.Limit.HasColimits (i Data.Category.Coproduct.:>>: j) k
+ Data.Category.Limit: instance (Data.Category.Limit.HasTerminalObject c1, Data.Category.Limit.HasTerminalObject c2) => Data.Category.Limit.HasTerminalObject (c1 Data.Category.Product.:**: c2)
+ Data.Category.Limit: instance Data.Category.Category k => Data.Category.Limit.HasColimits Data.Category.Unit.Unit k
+ Data.Category.Limit: instance Data.Category.Category k => Data.Category.Limit.HasLimits Data.Category.Unit.Unit k
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Functor.Cat
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryCoproducts Data.Category.Unit.Unit
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryCoproducts k => Data.Category.Functor.Functor (Data.Category.Limit.CoproductFunctor k)
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryCoproducts k => Data.Category.Limit.HasBinaryProducts (Data.Category.Op k)
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryProducts (->)
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryProducts Data.Category.Functor.Cat
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryProducts Data.Category.Unit.Unit
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryProducts k => Data.Category.Functor.Functor (Data.Category.Limit.ProductFunctor k)
+ Data.Category.Limit: instance Data.Category.Limit.HasBinaryProducts k => Data.Category.Limit.HasBinaryCoproducts (Data.Category.Op k)
+ Data.Category.Limit: instance Data.Category.Limit.HasColimits j k => Data.Category.Functor.Functor (Data.Category.Limit.ColimitFunctor j k)
+ Data.Category.Limit: instance Data.Category.Limit.HasInitialObject (->)
+ Data.Category.Limit: instance Data.Category.Limit.HasInitialObject Data.Category.Functor.Cat
+ Data.Category.Limit: instance Data.Category.Limit.HasInitialObject Data.Category.Unit.Unit
+ Data.Category.Limit: instance Data.Category.Limit.HasInitialObject k => Data.Category.Limit.HasColimits Data.Category.Void.Void k
+ Data.Category.Limit: instance Data.Category.Limit.HasInitialObject k => Data.Category.Limit.HasTerminalObject (Data.Category.Op k)
+ Data.Category.Limit: instance Data.Category.Limit.HasLimits j k => Data.Category.Functor.Functor (Data.Category.Limit.LimitFunctor j k)
+ Data.Category.Limit: instance Data.Category.Limit.HasTerminalObject (->)
+ Data.Category.Limit: instance Data.Category.Limit.HasTerminalObject Data.Category.Functor.Cat
+ Data.Category.Limit: instance Data.Category.Limit.HasTerminalObject Data.Category.Unit.Unit
+ Data.Category.Limit: instance Data.Category.Limit.HasTerminalObject k => Data.Category.Limit.HasInitialObject (Data.Category.Op k)
+ Data.Category.Limit: instance Data.Category.Limit.HasTerminalObject k => Data.Category.Limit.HasLimits Data.Category.Void.Void k
+ Data.Category.Limit: type family BinaryCoproduct (k :: * -> * -> *) x y :: *;
+ Data.Category.Limit: }
+ Data.Category.Monoidal: [MonoidValue] :: (TensorProduct f, Dom f ~ (k :**: k), Cod f ~ k) => f -> MonoidObject f m -> k (Unit f) m -> MonoidAsCategory f m m m
+ Data.Category.Monoidal: [comultiply] :: ComonoidObject f a -> Cod f a (f :% (a, a))
+ Data.Category.Monoidal: [counit] :: ComonoidObject f a -> Cod f a (Unit f)
+ Data.Category.Monoidal: [multiply] :: MonoidObject f a -> Cod f ((f :% (a, a))) a
+ Data.Category.Monoidal: [unit] :: MonoidObject f a -> Cod f (Unit f) a
+ Data.Category.Monoidal: instance (Data.Category.Limit.HasInitialObject k, Data.Category.Limit.HasBinaryCoproducts k) => Data.Category.Monoidal.TensorProduct (Data.Category.Limit.CoproductFunctor k)
+ Data.Category.Monoidal: instance (Data.Category.Limit.HasTerminalObject k, Data.Category.Limit.HasBinaryProducts k) => Data.Category.Monoidal.TensorProduct (Data.Category.Limit.ProductFunctor k)
+ Data.Category.Monoidal: instance Data.Category.Category (Data.Category.Monoidal.MonoidAsCategory f m)
+ Data.Category.Monoidal: instance Data.Category.Category k => Data.Category.Monoidal.TensorProduct (Data.Category.NaturalTransformation.EndoFunctorCompose k)
+ Data.Category.Monoidal: type family Unit f :: *;
+ Data.Category.Monoidal: }
+ Data.Category.NNO: instance (Data.Category.Functor.Functor z, Data.Category.Functor.Functor s, Data.Category.Functor.Dom z ~ Data.Category.Unit.Unit, Data.Category.Functor.Cod z ~ Data.Category.Functor.Dom s, Data.Category.Functor.Dom s ~ Data.Category.Functor.Cod s) => Data.Category.Functor.Functor (Data.Category.NNO.PrimRec z s)
+ Data.Category.NNO: instance Data.Category.NNO.HasNaturalNumberObject (->)
+ Data.Category.NNO: instance Data.Category.NNO.HasNaturalNumberObject Data.Category.Functor.Cat
+ Data.Category.NNO: type family NaturalNumberObject k :: *;
+ Data.Category.NNO: }
+ Data.Category.NaturalTransformation: Apply :: Apply
+ Data.Category.NaturalTransformation: Tuple :: Tuple
+ Data.Category.NaturalTransformation: [Nat] :: (Functor f, Functor g, c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => f -> g -> (forall z. Obj c z -> Component f g z) -> Nat c d f g
+ Data.Category.NaturalTransformation: [unCom] :: Com f g z -> Component f g z
+ Data.Category.NaturalTransformation: data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *)
+ Data.Category.NaturalTransformation: data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *)
+ Data.Category.NaturalTransformation: infixl 9 !
+ Data.Category.NaturalTransformation: instance (Data.Category.Category c, Data.Category.Category d, Data.Category.Category e) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.FunctorCompose c d e)
+ Data.Category.NaturalTransformation: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Apply c1 c2)
+ Data.Category.NaturalTransformation: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Tuple c1 c2)
+ Data.Category.NaturalTransformation: instance (Data.Category.Functor.Functor f, Data.Category.Functor.Functor h) => Data.Category.Functor.Functor (Data.Category.NaturalTransformation.Wrap f h)
+ Data.Category.NaturalTransformation: instance Data.Category.Category d => Data.Category.Category (Data.Category.NaturalTransformation.Nat c d)
+ Data.Category.NaturalTransformation: type Presheaves k = Nat (Op k) (->)
+ Data.Category.Product: [:**:] :: c1 a1 b1 -> c2 a2 b2 -> (:**:) c1 c2 (a1, a2) (b1, b2)
+ Data.Category.Product: instance (Data.Category.Category c1, Data.Category.Category c2) => Data.Category.Category (c1 Data.Category.Product.:**: c2)
+ Data.Category.RepresentableFunctor: [represent] :: Representable f repObj -> forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z
+ Data.Category.RepresentableFunctor: [representedFunctor] :: Representable f repObj -> f
+ Data.Category.RepresentableFunctor: [representingObject] :: Representable f repObj -> Obj (Dom f) repObj
+ Data.Category.RepresentableFunctor: [universalElement] :: Representable f repObj -> forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj
+ Data.Category.Simplex: [Fs] :: Fin n -> Fin (S n)
+ Data.Category.Simplex: [Fz] :: Fin (S n)
+ Data.Category.Simplex: [X] :: Simplex x (S y) -> Simplex (S x) (S y)
+ Data.Category.Simplex: [Y] :: Simplex x y -> Simplex x (S y)
+ Data.Category.Simplex: [Z] :: Simplex Z Z
+ Data.Category.Simplex: instance Data.Category.Category Data.Category.Simplex.Simplex
+ Data.Category.Simplex: instance Data.Category.Functor.Functor Data.Category.Simplex.Add
+ Data.Category.Simplex: instance Data.Category.Functor.Functor Data.Category.Simplex.Forget
+ Data.Category.Simplex: instance Data.Category.Limit.HasInitialObject Data.Category.Simplex.Simplex
+ Data.Category.Simplex: instance Data.Category.Limit.HasTerminalObject Data.Category.Simplex.Simplex
+ Data.Category.Simplex: instance Data.Category.Monoidal.TensorProduct Data.Category.Simplex.Add
+ Data.Category.Simplex: instance Data.Category.Monoidal.TensorProduct f => Data.Category.Functor.Functor (Data.Category.Simplex.Replicate f a)
+ Data.Category.Unit: [Unit] :: Unit () ()
+ Data.Category.Unit: instance Data.Category.Category Data.Category.Unit.Unit
+ Data.Category.Void: instance Data.Category.Category Data.Category.Void.Void
+ Data.Category.Void: instance Data.Category.Category k => Data.Category.Functor.Functor (Data.Category.Void.Magic k)
+ Data.Category.Yoneda: instance (Data.Category.Category k, Data.Category.Functor.Functor f, Data.Category.Functor.Dom f ~ Data.Category.Op k, Data.Category.Functor.Cod f ~ (->)) => Data.Category.Functor.Functor (Data.Category.Yoneda.Yoneda k f)
- Data.Category.Adjunction: initialPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
+ Data.Category.Adjunction: initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g
- Data.Category.Adjunction: mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g
+ Data.Category.Adjunction: mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g
- Data.Category.Adjunction: terminalPropAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
+ Data.Category.Adjunction: terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g
- Data.Category.CartesianClosed: class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where type family Exponential k y z :: *
+ Data.Category.CartesianClosed: class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where type Exponential k y z :: * where {
- Data.Category.Comma: initialUniversalComma :: (Functor u, c ~ (u ObjectsFUnder x), HasInitialObject c, (a_, a) ~ InitialObject c) => u -> InitialUniversal x u a
+ Data.Category.Comma: initialUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFUnder` x), HasInitialObject c, (a_, a) ~ InitialObject c) => u -> InitialUniversal x u a
- Data.Category.Comma: terminalUniversalComma :: (Functor u, c ~ (u ObjectsFOver x), HasTerminalObject c, (a, a_) ~ TerminalObject c) => u -> TerminalUniversal x u a
+ Data.Category.Comma: terminalUniversalComma :: forall u x c a a_. (Functor u, c ~ (u `ObjectsFOver` x), HasTerminalObject c, (a, a_) ~ TerminalObject c) => u -> TerminalUniversal x u a
- Data.Category.Comma: type ObjectsOver c a = Id c ObjectsFOver a
+ Data.Category.Comma: type ObjectsOver c a = Id c `ObjectsFOver` a
- Data.Category.Comma: type ObjectsUnder c a = Id c ObjectsFUnder a
+ Data.Category.Comma: type ObjectsUnder c a = Id c `ObjectsFUnder` a
- Data.Category.Coproduct: (:+++:) :: f1 -> f2 -> :+++: f1 f2
+ Data.Category.Coproduct: (:+++:) :: f1 -> f2 -> (:+++:) f1 f2
- Data.Category.Fix: type Omega = Fix (:>>: Unit)
+ Data.Category.Fix: type Omega = Fix ((:>>:) Unit)
- Data.Category.Functor: (:***:) :: f1 -> f2 -> :***: f1 f2
+ Data.Category.Functor: (:***:) :: f1 -> f2 -> (:***:) f1 f2
- Data.Category.Functor: class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where type family Dom ftag :: * -> * -> * type family Cod ftag :: * -> * -> * type family (:%) ftag a :: *
+ Data.Category.Functor: class (Category (Dom ftag), Category (Cod ftag)) => Functor ftag where type Dom ftag :: * -> * -> * type Cod ftag :: * -> * -> * type (:%) ftag a :: * where {
- Data.Category.Limit: class Category k => HasBinaryCoproducts k where type family BinaryCoproduct (k :: * -> * -> *) x y :: * l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)
+ Data.Category.Limit: class Category k => HasBinaryCoproducts k where type BinaryCoproduct (k :: * -> * -> *) x y :: * l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r) where {
- Data.Category.Limit: class Category k => HasBinaryProducts k where type family BinaryProduct (k :: * -> * -> *) x y :: * l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r))
+ Data.Category.Limit: class Category k => HasBinaryProducts k where type BinaryProduct (k :: * -> * -> *) x y :: * l *** r = (l . proj1 (src l) (src r)) &&& (r . proj2 (src l) (src r)) where {
- Data.Category.Limit: class Category k => HasInitialObject k where type family InitialObject k :: *
+ Data.Category.Limit: class Category k => HasInitialObject k where type InitialObject k :: * where {
- Data.Category.Limit: class Category k => HasTerminalObject k where type family TerminalObject k :: *
+ Data.Category.Limit: class Category k => HasTerminalObject k where type TerminalObject k :: * where {
- Data.Category.Limit: colimitAdj :: HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
+ Data.Category.Limit: colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k)
- Data.Category.Limit: limitAdj :: HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
+ Data.Category.Limit: limitAdj :: forall j k. HasLimits j k => Adjunction (Nat j k) k (Diag j k) (LimitFunctor j k)
- Data.Category.Monoidal: ComonoidObject :: (forall k. Cod f ~ k => k a (Unit f)) -> (forall k. Cod f ~ k => k a (f :% (a, a))) -> ComonoidObject f a
+ Data.Category.Monoidal: ComonoidObject :: Cod f a (Unit f) -> Cod f a (f :% (a, a)) -> ComonoidObject f a
- Data.Category.Monoidal: MonoidObject :: (forall k. Cod f ~ k => k (Unit f) a) -> (forall k. Cod f ~ k => k ((f :% (a, a))) a) -> MonoidObject f a
+ Data.Category.Monoidal: MonoidObject :: Cod f (Unit f) a -> Cod f ((f :% (a, a))) a -> MonoidObject f a
- Data.Category.Monoidal: class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where type family Unit f :: *
+ Data.Category.Monoidal: class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where type Unit f :: * where {
- Data.Category.Monoidal: mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) => f -> (forall a. Obj k a -> Component f (Id k) a) -> (forall a. Obj k a -> Component f (f :.: f) a) -> Comonad f
+ Data.Category.Monoidal: mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k) => f -> (forall a. Obj k a -> Component f (Id k) a) -> (forall a. Obj k a -> Component f (f :.: f) a) -> Comonad f
- Data.Category.Monoidal: mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) => f -> (forall a. Obj k a -> Component (Id k) f a) -> (forall a. Obj k a -> Component (f :.: f) f a) -> Monad f
+ Data.Category.Monoidal: mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k) => f -> (forall a. Obj k a -> Component (Id k) f a) -> (forall a. Obj k a -> Component (f :.: f) f a) -> Monad f
- Data.Category.NNO: class HasTerminalObject k => HasNaturalNumberObject k where type family NaturalNumberObject k :: *
+ Data.Category.NNO: class HasTerminalObject k => HasNaturalNumberObject k where type NaturalNumberObject k :: * where {
- Data.Category.NNO: type Nat = Fix (:++: Unit)
+ Data.Category.NNO: type Nat = Fix ((:++:) Unit)
- Data.Category.NaturalTransformation: type (:~>) f g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
+ Data.Category.NaturalTransformation: type (:~>) f g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g
- Data.Category.Void: voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g
+ Data.Category.Void: voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g
- Data.Category.Yoneda: fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f
+ Data.Category.Yoneda: fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f
- Data.Category.Yoneda: toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f
+ Data.Category.Yoneda: toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f)
Files
- Data/Category/Adjunction.hs +20/−20
- Data/Category/Boolean.hs +15/−19
- Data/Category/CartesianClosed.hs +33/−23
- Data/Category/Limit.hs +75/−73
- Data/Category/Monoidal.hs +24/−24
- Data/Category/NaturalTransformation.hs +36/−14
- Data/Category/Presheaf.hs +0/−39
- Data/Category/RepresentableFunctor.hs +9/−9
- Data/Category/Void.hs +3/−3
- Data/Category/Yoneda.hs +6/−7
- data-category.cabal +1/−2
Data/Category/Adjunction.hs view
@@ -16,27 +16,27 @@ , leftAdjunct , rightAdjunct- + -- * Adjunctions as a category , idAdj , composeAdj , AdjArrow(..)- + -- * Adjunctions from universal morphisms , initialPropAdjunction , terminalPropAdjunction- + -- * Universal morphisms from adjunctions , adjunctionInitialProp , adjunctionTerminalProp- + -- * Examples , precomposeAdj , postcomposeAdj , contAdj- + ) where- + import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -50,9 +50,9 @@ , counit :: Nat c c (f :.: g) (Id c) } -mkAdjunction :: (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)- => f -> g - -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) +mkAdjunction :: (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+ => f -> g+ -> (forall a. Obj d a -> Component (Id d) (g :.: f) a) -> (forall a. Obj c a -> Component (f :.: g) (Id c) a) -> Adjunction c d f g mkAdjunction f g un coun = Adjunction f g (Nat Id (g :.: f) un) (Nat (f :.: g) Id coun)@@ -74,24 +74,24 @@ -initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)+initialPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall y. Obj d y -> InitialUniversal y g (f :% y)) -> Adjunction c d f g-initialPropAdjunction f g univ = mkAdjunction f g +initialPropAdjunction f g univ = mkAdjunction f g (universalElement . univ) (\a -> represent (univ (g % a)) a (g % a))- -terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Category c, Category d, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d)++terminalPropAdjunction :: forall f g c d. (Functor f, Functor g, Dom f ~ d, Cod f ~ c, Dom g ~ c, Cod g ~ d) => f -> g -> (forall x. Obj c x -> TerminalUniversal x f (g :% x)) -> Adjunction c d f g-terminalPropAdjunction f g univ = mkAdjunction f g +terminalPropAdjunction f g univ = mkAdjunction f g (\a -> unOp (represent (univ (f % a)) (Op a) (f % a))) (universalElement . univ)- + idAdj :: Category k => Adjunction k k (Id k) (Id k) idAdj = mkAdjunction Id Id (\x -> x) (\x -> x) composeAdj :: Adjunction d e f g -> Adjunction c d f' g' -> Adjunction c e (f' :.: f) (g :.: g')-composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g') +composeAdj (Adjunction f g u c) (Adjunction f' g' u' c') = Adjunction (f' :.: f) (g :.: g') (compAssoc (g :.: g') f' f . precompose f % (compAssocInv g g' f' . postcompose g % u' . idPrecompInv g) . u) (c' . precompose g' % (idPrecomp f' . postcompose f' % c . compAssoc f' f g) . compAssocInv (f' :.: f) g g') @@ -101,23 +101,23 @@ -- | The category with categories as objects and adjunctions as arrows. instance Category AdjArrow where- + src (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj tgt (AdjArrow (Adjunction _ _ _ _)) = AdjArrow idAdj- + AdjArrow x . AdjArrow y = AdjArrow (composeAdj x y) precomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat c e) (Nat d e) (Precompose g e) (Precompose f e)-precomposeAdj (Adjunction f g un coun) = mkAdjunction +precomposeAdj (Adjunction f g un coun) = mkAdjunction (precompose g) (precompose f) (\nh@(Nat h _ _) -> compAssocInv h g f . (nh `o` un) . idPrecompInv h) (\nh@(Nat h _ _) -> idPrecomp h . (nh `o` coun) . compAssoc h f g) postcomposeAdj :: Category e => Adjunction c d f g -> Adjunction (Nat e c) (Nat e d) (Postcompose f e) (Postcompose g e)-postcomposeAdj (Adjunction f g un coun) = mkAdjunction +postcomposeAdj (Adjunction f g un coun) = mkAdjunction (postcompose f) (postcompose g) (\nh@(Nat h _ _) -> compAssoc g f h . (un `o` nh) . idPostcompInv h)
Data/Category/Boolean.hs view
@@ -15,9 +15,6 @@ module Data.Category.Boolean where import Data.Category-import Data.Category.Functor-import Data.Category.NaturalTransformation-import Data.Category.Product import Data.Category.Limit import Data.Category.Monoidal import Data.Category.CartesianClosed@@ -25,7 +22,7 @@ data Fls data Tru- + data Boolean a b where Fls :: Boolean Fls Fls F2T :: Boolean Fls Tru@@ -33,15 +30,15 @@ -- | @Boolean@ is the category with true and false as objects, and an arrow from false to true. instance Category Boolean where- + src Fls = Fls src F2T = Fls src Tru = Tru- + tgt Fls = Fls tgt F2T = Tru tgt Tru = Tru- + Fls . Fls = Fls F2T . Fls = F2T Tru . F2T = F2T@@ -54,7 +51,7 @@ initialObject = Fls initialize Fls = Fls initialize Tru = F2T- + -- | True is the terminal object in the Boolean category. instance HasTerminalObject Boolean where type TerminalObject Boolean = Tru@@ -65,12 +62,12 @@ -- | Conjunction is the binary product in the Boolean category. instance HasBinaryProducts Boolean where- + type BinaryProduct Boolean Fls Fls = Fls type BinaryProduct Boolean Fls Tru = Fls type BinaryProduct Boolean Tru Fls = Fls type BinaryProduct Boolean Tru Tru = Tru- + proj1 Fls Fls = Fls proj1 Fls Tru = Fls proj1 Tru Fls = F2T@@ -79,7 +76,7 @@ proj2 Fls Tru = F2T proj2 Tru Fls = Fls proj2 Tru Tru = Tru- + Fls &&& Fls = Fls Fls &&& F2T = Fls F2T &&& Fls = Fls@@ -89,12 +86,12 @@ -- | Disjunction is the binary coproduct in the Boolean category. instance HasBinaryCoproducts Boolean where- + type BinaryCoproduct Boolean Fls Fls = Fls type BinaryCoproduct Boolean Fls Tru = Tru type BinaryCoproduct Boolean Tru Fls = Tru type BinaryCoproduct Boolean Tru Tru = Tru- + inj1 Fls Fls = Fls inj1 Fls Tru = F2T inj1 Tru Fls = Tru@@ -103,7 +100,7 @@ inj2 Fls Tru = Tru inj2 Tru Fls = F2T inj2 Tru Tru = Tru- + Fls ||| Fls = Fls F2T ||| F2T = F2T F2T ||| Tru = Tru@@ -113,22 +110,22 @@ -- | Implication makes the Boolean category cartesian closed. instance CartesianClosed Boolean where- + type Exponential Boolean Fls Fls = Tru type Exponential Boolean Fls Tru = Tru type Exponential Boolean Tru Fls = Fls type Exponential Boolean Tru Tru = Tru- + apply Fls Fls = Fls apply Fls Tru = F2T apply Tru Fls = Fls apply Tru Tru = Tru- + tuple Fls Fls = F2T tuple Fls Tru = Tru tuple Tru Fls = Fls tuple Tru Tru = Tru- + Fls ^^^ Fls = Tru Fls ^^^ F2T = F2T Fls ^^^ Tru = Fls@@ -157,4 +154,3 @@ falseProductComonoid :: ComonoidObject (ProductFunctor Boolean) Fls falseProductComonoid = ComonoidObject F2T Fls-
Data/Category/CartesianClosed.hs view
@@ -1,4 +1,13 @@-{-# LANGUAGE TypeOperators, TypeFamilies, GADTs, Rank2Types, ScopedTypeVariables, UndecidableInstances, TypeSynonymInstances, NoImplicitPrelude #-}+{-# LANGUAGE+ TypeOperators,+ TypeFamilies,+ GADTs,+ Rank2Types,+ ScopedTypeVariables,+ UndecidableInstances,+ TypeSynonymInstances,+ FlexibleInstances,+ NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Category.CartesianClosed@@ -9,7 +18,7 @@ -- Portability : non-portable ----------------------------------------------------------------------------- module Data.Category.CartesianClosed where- + import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation@@ -17,12 +26,13 @@ import Data.Category.Limit import Data.Category.Adjunction import Data.Category.Monoidal as M+import Data.Category.Yoneda -- | A category is cartesian closed if it has all products and exponentials for all objects. class (HasTerminalObject k, HasBinaryProducts k) => CartesianClosed k where type Exponential k y z :: *- + apply :: Obj k y -> Obj k z -> k (BinaryProduct k (Exponential k y z) y) z tuple :: Obj k y -> Obj k z -> k z (Exponential k y (BinaryProduct k z y)) (^^^) :: k z1 z2 -> k y2 y1 -> k (Exponential k y1 z1) (Exponential k y2 z2)@@ -41,39 +51,40 @@ -- | Exponentials in @Hask@ are functions. instance CartesianClosed (->) where type Exponential (->) y z = y -> z- + apply _ _ (f, y) = f y tuple _ _ z = \y -> (z, y) f ^^^ h = \g -> f . g . h -data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply--- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.-instance (Category c1, Category c2) => Functor (Apply c1 c2) where- type Dom (Apply c1 c2) = Nat c2 c1 :**: c2- type Cod (Apply c1 c2) = c1- type Apply c1 c2 :% (f, a) = f :% a- Apply % (l :**: r) = l ! r--data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple--- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@.-instance (Category c1, Category c2) => Functor (Tuple c1 c2) where- type Dom (Tuple c1 c2) = c1- type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)- type Tuple c1 c2 :% a = Tuple1 c1 c2 a- Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)-- -- | Exponentials in @Cat@ are the functor categories. instance CartesianClosed Cat where type Exponential Cat (CatW c) (CatW d) = CatW (Nat c d)- + apply CatA{} CatA{} = CatA Apply tuple CatA{} CatA{} = CatA Tuple (CatA f) ^^^ (CatA h) = CatA (Wrap f h) +type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite+ ( ProductFunctor (Presheaves k)+ :.: Tuple2 (Presheaves k) (Presheaves k) y+ :.: YonedaEmbedding k+ )+pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z+pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: tuple2 y :.: yonedaEmbedding)++-- | The category of presheaves on a category @C@ is cartesian closed for any @C@.+instance Category k => CartesianClosed (Presheaves k) where+ type Exponential (Presheaves k) y z = PShExponential k y z++ apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))+ tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))+ zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))+++ -- | The product functor is left adjoint the the exponential functor. curryAdj :: CartesianClosed k => Obj k y@@ -107,4 +118,3 @@ contextComonadDuplicate :: CartesianClosed k => Obj k s -> Obj k a -> k (Context k s a) (Context k s (Context k s a)) contextComonadDuplicate s a = M.comultiply (adjunctionComonad (curryAdj s)) ! a-
Data/Category/Limit.hs view
@@ -22,36 +22,36 @@ module Data.Category.Limit ( -- * Preliminairies- + -- ** Diagonal Functor Diag(..) , DiagF- + -- ** Cones , Cone , Cocone , coneVertex , coconeVertex- + -- * Limits , LimitFam , Limit , HasLimits(..) , LimitFunctor(..) , limitAdj- + -- * Colimits , ColimitFam , Colimit , HasColimits(..) , ColimitFunctor(..) , colimitAdj- + -- ** Limits of type Void , HasTerminalObject(..) , HasInitialObject(..) , Zero- + -- ** Limits of type Pair , HasBinaryProducts(..) , ProductFunctor(..)@@ -61,7 +61,7 @@ , CoproductFunctor(..) , (:+:)(..) , coprodAdj- + ) where import Data.Category@@ -82,13 +82,13 @@ data Diag :: (* -> * -> *) -> (* -> * -> *) -> * where Diag :: Diag j k- + -- | The diagonal functor from (index-) category J to k. instance (Category j, Category k) => Functor (Diag j k) where type Dom (Diag j k) = k type Cod (Diag j k) = Nat j k type Diag j k :% a = Const j k a- + Diag % f = Nat (Const (src f)) (Const (tgt f)) (\_ -> f) -- | The diagonal functor with the same domain and codomain as @f@.@@ -170,15 +170,15 @@ colimitAdj :: forall j k. HasColimits j k => Adjunction k (Nat j k) (ColimitFunctor j k) (Diag j k) colimitAdj = mkAdjunction ColimitFunctor diag (\f @ Nat{} -> colimit f) (\a -> colimitFactorizer (diag % a) (diag % a)) where diag = Diag :: Diag j k -- Forces the type of all Diags to be the same.- + class Category k => HasTerminalObject k where- + type TerminalObject k :: *- + terminalObject :: Obj k (TerminalObject k)- + terminate :: Obj k a -> k a (TerminalObject k) @@ -186,7 +186,7 @@ -- | A terminal object is the limit of the functor from /0/ to k. instance (HasTerminalObject k) => HasLimits Void k where- + limit (Nat f _ _) = voidNat (Const terminalObject) f limitFactorizer Nat{} = terminate . coneVertex @@ -194,49 +194,49 @@ -- | @()@ is the terminal object in @Hask@. instance HasTerminalObject (->) where type TerminalObject (->) = ()- + terminalObject = \x -> x- + terminate _ _ = () -- | @Unit@ is the terminal category. instance HasTerminalObject Cat where type TerminalObject Cat = CatW Unit- + terminalObject = CatA Id- + terminate (CatA _) = CatA (Const Unit) -- | The constant functor to the terminal object is itself the terminal object in its functor category. instance (Category c, HasTerminalObject d) => HasTerminalObject (Nat c d) where type TerminalObject (Nat c d) = Const c d (TerminalObject d)- + terminalObject = natId (Const terminalObject)- + terminate (Nat f _ _) = Nat f (Const terminalObject) (terminate . (f %)) -- | The category of one object has that object as terminal object. instance HasTerminalObject Unit where type TerminalObject Unit = ()- + terminalObject = Unit- + terminate Unit = Unit- + -- | The terminal object of the product of 2 categories is the product of their terminal objects. instance (HasTerminalObject c1, HasTerminalObject c2) => HasTerminalObject (c1 :**: c2) where type TerminalObject (c1 :**: c2) = (TerminalObject c1, TerminalObject c2)- + terminalObject = terminalObject :**: terminalObject- + terminate (a1 :**: a2) = terminate a1 :**: terminate a2- + -- | The terminal object of the direct coproduct of categories is the terminal object of the terminal category. instance (Category c1, HasTerminalObject c2) => HasTerminalObject (c1 :>>: c2) where type TerminalObject (c1 :>>: c2) = I2 (TerminalObject c2)- + terminalObject = I2A terminalObject- + terminate (I1A a) = I12 a terminalObject terminate (I2A a) = I2A (terminate a) @@ -244,7 +244,7 @@ class Category k => HasInitialObject k where type InitialObject k :: *- + initialObject :: Obj k (InitialObject k) initialize :: Obj k a -> k (InitialObject k) a@@ -254,7 +254,7 @@ -- | An initial object is the colimit of the functor from /0/ to k. instance HasInitialObject k => HasColimits Void k where- + colimit (Nat f _ _) = voidNat f (Const initialObject) colimitFactorizer Nat{} = initialize . coconeVertex @@ -264,56 +264,56 @@ -- | Any empty data type is an initial object in @Hask@. instance HasInitialObject (->) where type InitialObject (->) = Zero- + initialObject = \x -> x- + initialize = initialize -- | The empty category is the initial object in @Cat@. instance HasInitialObject Cat where type InitialObject Cat = CatW Void- + initialObject = CatA Id- + initialize (CatA _) = CatA Magic -- | The constant functor to the initial object is itself the initial object in its functor category. instance (Category c, HasInitialObject d) => HasInitialObject (Nat c d) where type InitialObject (Nat c d) = Const c d (InitialObject d)- + initialObject = natId (Const initialObject)- + initialize (Nat f _ _) = Nat (Const initialObject) f (initialize . (f %)) -- | The initial object of the product of 2 categories is the product of their initial objects. instance (HasInitialObject c1, HasInitialObject c2) => HasInitialObject (c1 :**: c2) where type InitialObject (c1 :**: c2) = (InitialObject c1, InitialObject c2)- + initialObject = initialObject :**: initialObject- + initialize (a1 :**: a2) = initialize a1 :**: initialize a2 -- | The category of one object has that object as initial object. instance HasInitialObject Unit where type InitialObject Unit = ()- + initialObject = Unit- + initialize Unit = Unit -- | The initial object of the direct coproduct of categories is the initial object of the initial category. instance (HasInitialObject c1, Category c2) => HasInitialObject (c1 :>>: c2) where type InitialObject (c1 :>>: c2) = I1 (InitialObject c1)- + initialObject = I1A initialObject- + initialize (I1A a) = I1A (initialize a) initialize (I2A a) = I12 initialObject a class Category k => HasBinaryProducts k where type BinaryProduct (k :: * -> * -> *) x y :: *- + proj1 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) x proj2 :: Obj k x -> Obj k y -> k (BinaryProduct k x y) y @@ -329,7 +329,7 @@ -- | If `k` has binary products, we can take the limit of 2 joined diagrams. instance (HasLimits i k, HasLimits j k, HasBinaryProducts k) => HasLimits (i :++: j) k where- + limit = limit' where limit' :: forall f. Obj (Nat (i :++: j) k) f -> Cone f (Limit f)@@ -352,20 +352,20 @@ -- | The tuple is the binary product in @Hask@. instance HasBinaryProducts (->) where type BinaryProduct (->) x y = (x, y)- + proj1 _ _ = \(x, _) -> x proj2 _ _ = \(_, y) -> y- + f &&& g = \x -> (f x, g x) f *** g = \(x, y) -> (f x, g y) -- | The product of categories ':**:' is the binary product in 'Cat'. instance HasBinaryProducts Cat where type BinaryProduct Cat (CatW c1) (CatW c2) = CatW (c1 :**: c2)- + proj1 (CatA _) (CatA _) = CatA Proj1 proj2 (CatA _) (CatA _) = CatA Proj2- + CatA f1 &&& CatA f2 = CatA ((f1 :***: f2) :.: DiagProd) CatA f1 *** CatA f2 = CatA (f1 :***: f2) @@ -375,17 +375,17 @@ proj1 Unit Unit = Unit proj2 Unit Unit = Unit- + Unit &&& Unit = Unit Unit *** Unit = Unit -- | The binary product of the product of 2 categories is the product of their binary products. instance (HasBinaryProducts c1, HasBinaryProducts c2) => HasBinaryProducts (c1 :**: c2) where type BinaryProduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryProduct c1 x1 y1, BinaryProduct c2 x2 y2)- + proj1 (x1 :**: x2) (y1 :**: y2) = proj1 x1 y1 :**: proj1 x2 y2 proj2 (x1 :**: x2) (y1 :**: y2) = proj2 x1 y1 :**: proj2 x2 y2- + (f1 :**: f2) &&& (g1 :**: g2) = (f1 &&& g1) :**: (f2 &&& g2) (f1 :**: f2) *** (g1 :**: g2) = (f1 *** g1) :**: (f2 *** g2) @@ -394,12 +394,12 @@ type BinaryProduct (c1 :>>: c2) (I1 a) (I2 b) = I1 a type BinaryProduct (c1 :>>: c2) (I2 a) (I1 b) = I1 b type BinaryProduct (c1 :>>: c2) (I2 a) (I2 b) = I2 (BinaryProduct c2 a b)- + proj1 (I1A a) (I1A b) = I1A (proj1 a b) proj1 (I1A a) (I2A _) = I1A a proj1 (I2A a) (I1A b) = I12 b a proj1 (I2A a) (I2A b) = I2A (proj1 a b)- + proj2 (I1A a) (I1A b) = I1A (proj2 a b) proj2 (I1A a) (I2A b) = I12 a b proj2 (I2A _) (I1A b) = I1A b@@ -409,6 +409,7 @@ I1A a &&& I12 _ _ = I1A a I12 _ _ &&& I1A b = I1A b I2A a &&& I2A b = I2A (a &&& b)+ I12 a b1 &&& I12 _ b2 = I12 a (b1 *** b2) data ProductFunctor (k :: * -> * -> *) = ProductFunctor@@ -437,15 +438,15 @@ -- | The functor product ':*:' is the binary product in functor categories. instance (Category c, HasBinaryProducts d) => HasBinaryProducts (Nat c d) where type BinaryProduct (Nat c d) x y = x :*: y- + proj1 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) f (\z -> proj1 (f % z) (g % z)) proj2 (Nat f _ _) (Nat g _ _) = Nat (f :*: g) g (\z -> proj2 (f % z) (g % z))- + Nat a f af &&& Nat _ g ag = Nat a (f :*: g) (\z -> af z &&& ag z) Nat f1 f2 f *** Nat g1 g2 g = Nat (f1 :*: g1) (f2 :*: g2) (\z -> f z *** g z)- + class Category k => HasBinaryCoproducts k where type BinaryCoproduct (k :: * -> * -> *) x y :: * @@ -453,18 +454,18 @@ inj2 :: Obj k x -> Obj k y -> k y (BinaryCoproduct k x y) (|||) :: (k x a) -> (k y a) -> (k (BinaryCoproduct k x y) a)- + (+++) :: (k a1 b1) -> (k a2 b2) -> (k (BinaryCoproduct k a1 a2) (BinaryCoproduct k b1 b2)) l +++ r = (inj1 (tgt l) (tgt r) . l) ||| (inj2 (tgt l) (tgt r) . r)- + type instance ColimitFam (i :++: j) k f = BinaryCoproduct k (ColimitFam i k (f :.: Inj1 i j)) (ColimitFam j k (f :.: Inj2 i j)) -- | If `k` has binary coproducts, we can take the colimit of 2 joined diagrams. instance (HasColimits i k, HasColimits j k, HasBinaryCoproducts k) => HasColimits (i :++: j) k where- + colimit = colimit' where colimit' :: forall f. Obj (Nat (i :++: j) k) f -> Cocone f (Colimit f)@@ -477,7 +478,7 @@ h :: Obj (i :++: j) z -> Com f (ConstF f (ColimitFam (i :++: j) k f)) z h (I1 n) = Com (inj1 x y . col1 ! n) h (I2 n) = Com (inj2 x y . col2 ! n)- + colimitFactorizer l@Nat{} c = colimitFactorizer (l `o` natId Inj1) (constPostcomp (tgtF c) Inj1 . (c `o` natId Inj1)) |||@@ -487,30 +488,30 @@ -- | The coproduct of categories ':++:' is the binary coproduct in 'Cat'. instance HasBinaryCoproducts Cat where type BinaryCoproduct Cat (CatW c1) (CatW c2) = CatW (c1 :++: c2)- + inj1 (CatA _) (CatA _) = CatA Inj1 inj2 (CatA _) (CatA _) = CatA Inj2- + CatA f1 ||| CatA f2 = CatA (CodiagCoprod :.: (f1 :+++: f2)) CatA f1 +++ CatA f2 = CatA (f1 :+++: f2) -- | In the category of one object that object is its own coproduct. instance HasBinaryCoproducts Unit where type BinaryCoproduct Unit () () = ()- + inj1 Unit Unit = Unit inj2 Unit Unit = Unit- + Unit ||| Unit = Unit Unit +++ Unit = Unit- + -- | The binary coproduct of the product of 2 categories is the product of their binary coproducts. instance (HasBinaryCoproducts c1, HasBinaryCoproducts c2) => HasBinaryCoproducts (c1 :**: c2) where type BinaryCoproduct (c1 :**: c2) (x1, x2) (y1, y2) = (BinaryCoproduct c1 x1 y1, BinaryCoproduct c2 x2 y2)- + inj1 (x1 :**: x2) (y1 :**: y2) = inj1 x1 y1 :**: inj1 x2 y2 inj2 (x1 :**: x2) (y1 :**: y2) = inj2 x1 y1 :**: inj2 x2 y2- + (f1 :**: f2) ||| (g1 :**: g2) = (f1 ||| g1) :**: (f2 ||| g2) (f1 :**: f2) +++ (g1 :**: g2) = (f1 +++ g1) :**: (f2 +++ g2) @@ -534,6 +535,7 @@ I2A a ||| I12 _ _ = I2A a I12 _ _ ||| I2A b = I2A b I2A a ||| I2A b = I2A (a ||| b)+ I12 a1 b ||| I12 a2 _ = I12 (a1 +++ a2) b data CoproductFunctor (k :: * -> * -> *) = CoproductFunctor@@ -562,10 +564,10 @@ -- | The functor coproduct ':+:' is the binary coproduct in functor categories. instance (Category c, HasBinaryCoproducts d) => HasBinaryCoproducts (Nat c d) where type BinaryCoproduct (Nat c d) x y = x :+: y- + inj1 (Nat f _ _) (Nat g _ _) = Nat f (f :+: g) (\z -> inj1 (f % z) (g % z)) inj2 (Nat f _ _) (Nat g _ _) = Nat g (f :+: g) (\z -> inj2 (f % z) (g % z))- + Nat f a fa ||| Nat g _ ga = Nat (f :+: g) a (\z -> fa z ||| ga z) Nat f1 f2 f +++ Nat g1 g2 g = Nat (f1 :+: g1) (f2 :+: g2) (\z -> f z +++ g z) @@ -606,7 +608,7 @@ -- | The limit of a single object is that object. instance Category k => HasLimits Unit k where- + limit (Nat f _ _) = Nat (Const (f % Unit)) f (\Unit -> f % Unit) limitFactorizer Nat{} n = n ! Unit @@ -614,7 +616,7 @@ -- | The limit of any diagram with an initial object, has the limit at the initial object. instance (HasInitialObject (i :>>: j), Category k) => HasLimits (i :>>: j) k where- + limit (Nat f _ _) = Nat (Const (f % initialObject)) f (\z -> f % initialize z) limitFactorizer Nat{} n = n ! initialObject @@ -623,10 +625,10 @@ -- | The colimit of a single object is that object. instance Category k => HasColimits Unit k where- + colimit (Nat f _ _) = Nat f (Const (f % Unit)) (\Unit -> f % Unit) colimitFactorizer Nat{} n = n ! Unit- + type instance ColimitFam (i :>>: j) k f = f :% TerminalObject (i :>>: j) -- | The colimit of any diagram with a terminal object, has the limit at the terminal object.
Data/Category/Monoidal.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE +{-# LANGUAGE TypeOperators , TypeFamilies , GADTs@@ -6,7 +6,7 @@ , ViewPatterns , TypeSynonymInstances , FlexibleInstances- , NoImplicitPrelude + , NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- |@@ -30,7 +30,7 @@ -- | A monoidal category is a category with some kind of tensor product. -- A tensor product is a bifunctor, with a unit object. class (Functor f, Dom f ~ (Cod f :**: Cod f)) => TensorProduct f where- + type Unit f :: * unitObject :: f -> Obj (Cod f) (Unit f) @@ -38,7 +38,7 @@ leftUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (Unit f, a)) rightUnitor :: Cod f ~ k => f -> Obj k a -> k (f :% (a, Unit f)) a rightUnitorInv :: Cod f ~ k => f -> Obj k a -> k a (f :% (a, Unit f))- + associator :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (f :% (a, b), c)) (f :% (a, f :% (b, c))) associatorInv :: Cod f ~ k => f -> Obj k a -> Obj k b -> Obj k c -> k (f :% (a, f :% (b, c))) (f :% (f :% (a, b), c)) @@ -46,7 +46,7 @@ -- | If a category has all products, then the product functor makes it a monoidal category, -- with the terminal object as unit. instance (HasTerminalObject k, HasBinaryProducts k) => TensorProduct (ProductFunctor k) where- + type Unit (ProductFunctor k) = TerminalObject k unitObject _ = terminalObject @@ -61,7 +61,7 @@ -- | If a category has all coproducts, then the coproduct functor makes it a monoidal category, -- with the initial object as unit. instance (HasInitialObject k, HasBinaryCoproducts k) => TensorProduct (CoproductFunctor k) where- + type Unit (CoproductFunctor k) = InitialObject k unitObject _ = initialObject @@ -69,16 +69,16 @@ leftUnitorInv _ a = inj2 initialObject a rightUnitor _ a = a ||| initialize a rightUnitorInv _ a = inj1 a initialObject- + associator _ a b c = (a +++ inj1 b c) ||| (inj2 a (b +++ c) . inj2 b c) associatorInv _ a b c = (inj1 (a +++ b) c . inj1 a b) ||| (inj2 a b +++ c)- + -- | Functor composition makes the category of endofunctors monoidal, with the identity functor as unit. instance Category k => TensorProduct (EndoFunctorCompose k) where- + type Unit (EndoFunctorCompose k) = Id k unitObject _ = natId Id- + leftUnitor _ (Nat g _ _) = idPostcomp g leftUnitorInv _ (Nat g _ _) = idPostcompInv g rightUnitor _ (Nat g _ _) = idPrecomp g@@ -90,10 +90,10 @@ -- | @MonoidObject f a@ defines a monoid @a@ in a monoidal category with tensor product @f@. data MonoidObject f a = MonoidObject- { unit :: (Cod f ~ k) => k (Unit f) a- , multiply :: (Cod f ~ k) => k ((f :% (a, a))) a+ { unit :: Cod f (Unit f) a+ , multiply :: Cod f ((f :% (a, a))) a }- + trivialMonoid :: TensorProduct f => f -> MonoidObject f (Unit f) trivialMonoid f = MonoidObject (unitObject f) (leftUnitor f (unitObject f)) @@ -103,13 +103,13 @@ -- | @ComonoidObject f a@ defines a comonoid @a@ in a comonoidal category with tensor product @f@. data ComonoidObject f a = ComonoidObject- { counit :: (Cod f ~ k) => k a (Unit f)- , comultiply :: (Cod f ~ k) => k a (f :% (a, a))+ { counit :: Cod f a (Unit f)+ , comultiply :: Cod f a (f :% (a, a)) } trivialComonoid :: TensorProduct f => f -> ComonoidObject f (Unit f) trivialComonoid f = ComonoidObject (unitObject f) (leftUnitorInv f (unitObject f))- + productComonoid :: (HasTerminalObject k, HasBinaryProducts k) => Obj k a -> ComonoidObject (ProductFunctor k) a productComonoid a = ComonoidObject (terminate a) (a &&& a) @@ -120,19 +120,19 @@ -- | A monoid as a category with one object. instance Category (MonoidAsCategory f m) where- + src (MonoidValue f m _) = MonoidValue f m (unit m) tgt (MonoidValue f m _) = MonoidValue f m (unit m)- + MonoidValue f m a . MonoidValue _ _ b = MonoidValue f m (multiply m . f % (a :**: b) . leftUnitorInv f (unitObject f)) -- | A monad is a monoid in the category of endofunctors. type Monad f = MonoidObject (EndoFunctorCompose (Dom f)) f -mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) - => f - -> (forall a. Obj k a -> Component (Id k) f a) +mkMonad :: (Functor f, Dom f ~ k, Cod f ~ k)+ => f+ -> (forall a. Obj k a -> Component (Id k) f a) -> (forall a. Obj k a -> Component (f :.: f) f a) -> Monad f mkMonad f ret join = MonoidObject@@ -147,9 +147,9 @@ -- | A comonad is a comonoid in the category of endofunctors. type Comonad f = ComonoidObject (EndoFunctorCompose (Dom f)) f -mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k, Category k) - => f - -> (forall a. Obj k a -> Component f (Id k) a) +mkComonad :: (Functor f, Dom f ~ k, Cod f ~ k)+ => f+ -> (forall a. Obj k a -> Component f (Id k) a) -> (forall a. Obj k a -> Component f (f :.: f) a) -> Comonad f mkComonad f extr dupl = ComonoidObject
Data/Category/NaturalTransformation.hs view
@@ -23,7 +23,8 @@ -- * Functor category , Nat(..) , Endo- + , Presheaves+ -- * Functor isomorphisms , compAssoc , compAssocInv@@ -35,7 +36,7 @@ , constPrecompInv , constPostcomp , constPostcompInv- + -- * Related functors , FunctorCompose(..) , EndoFunctorCompose@@ -44,9 +45,11 @@ , Postcompose , postcompose , Wrap(..)- + , Apply(..)+ , Tuple(..)+ ) where- + import Data.Category import Data.Category.Functor import Data.Category.Product@@ -54,7 +57,7 @@ infixl 9 ! -- | @f :~> g@ is a natural transformation from functor f to functor g.-type f :~> g = (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g+type f :~> g = forall c d. (c ~ Dom f, c ~ Dom g, d ~ Cod f, d ~ Cod g) => Nat c d f g -- | Natural transformations are built up of components, -- one for each object @z@ in the domain category of @f@ and @g@.@@ -94,11 +97,11 @@ -- | Functor category D^C. -- Objects of D^C are functors from C to D. -- Arrows of D^C are natural transformations.-instance (Category c, Category d) => Category (Nat c d) where- +instance Category d => Category (Nat c d) where+ src (Nat f _ _) = natId f tgt (Nat _ g _) = natId g- + Nat _ h ngh . Nat f _ nfg = Nat f h (\i -> ngh i . nfg i) @@ -123,19 +126,19 @@ idPostcompInv f = Nat f (Id :.: f) (f %) -constPrecomp :: (Category c1, Functor f) +constPrecomp :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (f :.: Const c1 (Dom f) x) (Const c1 (Cod f) (f :% x)) constPrecomp (Const x) f = let fx = f % x in Nat (f :.: Const x) (Const fx) (\_ -> fx) -constPrecompInv :: (Category c1, Functor f) +constPrecompInv :: (Category c1, Functor f) => Const c1 (Dom f) x -> f -> Nat c1 (Cod f) (Const c1 (Cod f) (f :% x)) (f :.: Const c1 (Dom f) x) constPrecompInv (Const x) f = let fx = f % x in Nat (Const fx) (f :.: Const x) (\_ -> fx) -constPostcomp :: (Category c2, Functor f) +constPostcomp :: (Category c2, Functor f) => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Cod f) c2 x :.: f) (Const (Dom f) c2 x) constPostcomp (Const x) f = Nat (Const x :.: f) (Const x) (\_ -> x) -constPostcompInv :: (Category c2, Functor f) +constPostcompInv :: (Category c2, Functor f) => Const (Cod f) c2 x -> f -> Nat (Dom f) c2 (Const (Dom f) c2 x) (Const (Cod f) c2 x :.: f) constPostcompInv (Const x) f = Nat (Const x) (Const x :.: f) (\_ -> x) @@ -147,7 +150,7 @@ type Dom (FunctorCompose c d e) = Nat d e :**: Nat c d type Cod (FunctorCompose c d e) = Nat c e type FunctorCompose c d e :% (f, g) = f :.: g- + FunctorCompose % (n1 :**: n2) = n1 `o` n2 @@ -156,6 +159,8 @@ -- | Composition of endofunctors is a functor. type EndoFunctorCompose k = FunctorCompose k k k +type Presheaves k = Nat (Op k) (->)+ -- | @Precompose f e@ is the functor such that @Precompose f e :% g = g :.: f@, -- for functors @g@ that compose with @f@ and with codomain @e@. type Precompose f e = FunctorCompose (Dom f) (Cod f) e :.: Tuple2 (Nat (Cod f) e) (Nat (Dom f) (Cod f)) f@@ -177,5 +182,22 @@ type Dom (Wrap f h) = Nat (Cod h) (Dom f) type Cod (Wrap f h) = Nat (Dom h) (Cod f) type Wrap f h :% g = f :.: g :.: h- + Wrap f h % n = natId f `o` n `o` natId h+++data Apply (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Apply+-- | 'Apply' is a bifunctor, @Apply :% (f, a)@ applies @f@ to @a@, i.e. @f :% a@.+instance (Category c1, Category c2) => Functor (Apply c1 c2) where+ type Dom (Apply c1 c2) = Nat c2 c1 :**: c2+ type Cod (Apply c1 c2) = c1+ type Apply c1 c2 :% (f, a) = f :% a+ Apply % (l :**: r) = l ! r++data Tuple (c1 :: * -> * -> *) (c2 :: * -> * -> *) = Tuple+-- | 'Tuple' converts an object @a@ to the functor 'Tuple1' @a@.+instance (Category c1, Category c2) => Functor (Tuple c1 c2) where+ type Dom (Tuple c1 c2) = c1+ type Cod (Tuple c1 c2) = Nat c2 (c1 :**: c2)+ type Tuple c1 c2 :% a = Tuple1 c1 c2 a+ Tuple % f = Nat (Tuple1 (src f)) (Tuple1 (tgt f)) (\z -> f :**: z)
− Data/Category/Presheaf.hs
@@ -1,39 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, TypeSynonymInstances, GADTs, FlexibleInstances, UndecidableInstances, NoImplicitPrelude #-}--------------------------------------------------------------------------------- |--- Module : Data.Category.Presheaf--- License : BSD-style (see the file LICENSE)------ Maintainer : sjoerd@w3future.com--- Stability : experimental--- Portability : non-portable-------------------------------------------------------------------------------module Data.Category.Presheaf where--import Data.Category-import Data.Category.Functor-import Data.Category.NaturalTransformation-import Data.Category.Limit-import Data.Category.CartesianClosed-import Data.Category.Yoneda---type Presheaves k = Nat (Op k) (->)--type PShExponential k y z = (Presheaves k :-*: z) :.: Opposite- ( ProductFunctor (Presheaves k)- :.: Tuple2 (Presheaves k) (Presheaves k) y- :.: YonedaEmbedding k- )-pshExponential :: Category k => Obj (Presheaves k) y -> Obj (Presheaves k) z -> PShExponential k y z-pshExponential y z = hom_X z :.: Opposite (ProductFunctor :.: tuple2 y :.: yonedaEmbedding)---- | The category of presheaves on a category @C@ is cartesian closed for any @C@.-instance Category k => CartesianClosed (Presheaves k) where- type Exponential (Presheaves k) y z = PShExponential k y z- - apply yn@(Nat y _ _) zn@(Nat z _ _) = Nat (pshExponential yn zn :*: y) z (\(Op i) (n, yi) -> (n ! Op i) (i, yi))- tuple yn zn@(Nat z _ _) = Nat z (pshExponential yn (zn *** yn)) (\(Op i) zi -> (Nat (hom_X i) z (\_ j2i -> (z % Op j2i) zi) *** yn))- zn ^^^ yn = Nat (pshExponential (tgt yn) (src zn)) (pshExponential (src yn) (tgt zn)) (\(Op i) n -> zn . n . (natId (hom_X i) *** yn))--
Data/Category/RepresentableFunctor.hs view
@@ -17,8 +17,8 @@ data Representable f repObj = Representable { representedFunctor :: f , representingObject :: Obj (Dom f) repObj- , represent :: (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z- , universalElement :: (Dom f ~ k, Cod f ~ (->)) => f :% repObj+ , represent :: forall k z. (Dom f ~ k, Cod f ~ (->)) => Obj k z -> f :% z -> k repObj z+ , universalElement :: forall k. (Dom f ~ k, Cod f ~ (->)) => f :% repObj } unrepresent :: (Functor f, Dom f ~ k, Cod f ~ (->)) => Representable f repObj -> k repObj z -> f :% z@@ -43,10 +43,10 @@ type InitialUniversal x u a = Representable ((x :*-: Cod u) :.: u) a -- | An initial universal property, a universal morphism from x to u. initialUniversal :: Functor u- => u - -> Obj (Dom u) a - -> Cod u x (u :% a) - -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) + => u+ -> Obj (Dom u) a+ -> Cod u x (u :% a)+ -> (forall y. Obj (Dom u) y -> Cod u x (u :% y) -> Dom u a y) -> InitialUniversal x u a initialUniversal u obj mor factorizer = Representable { representedFunctor = homX_ (src mor) :.: u@@ -54,14 +54,14 @@ , represent = factorizer , universalElement = mor }- + type TerminalUniversal x u a = Representable ((Cod u :-*: x) :.: Opposite u) a -- | A terminal universal property, a universal morphism from u to x. terminalUniversal :: Functor u- => u + => u -> Obj (Dom u) a -> Cod u (u :% a) x- -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) + -> (forall y. Obj (Dom u) y -> Cod u (u :% y) x -> Dom u y a) -> TerminalUniversal x u a terminalUniversal u obj mor factorizer = Representable { representedFunctor = hom_X (tgt mor) :.: Opposite u
Data/Category/Void.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, TypeFamilies, NoImplicitPrelude #-}+{-# LANGUAGE EmptyCase, LambdaCase, TypeOperators, GADTs, TypeFamilies, NoImplicitPrelude #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Category.Void@@ -18,7 +18,7 @@ data Void a b magic :: Void a b -> x-magic x = magic x+magic = \case { } -- | `Void` is the category with no objects. instance Category Void where@@ -29,7 +29,7 @@ (.) = magic -voidNat :: (Functor f, Functor g, Category d, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d)+voidNat :: (Functor f, Functor g, Dom f ~ Void, Dom g ~ Void, Cod f ~ d, Cod g ~ d) => f -> g -> Nat Void d f g voidNat f g = Nat f g magic
Data/Category/Yoneda.hs view
@@ -13,10 +13,9 @@ import Data.Category import Data.Category.Functor import Data.Category.NaturalTransformation-import Data.Category.CartesianClosed -type YonedaEmbedding k = - Postcompose (Hom k) (Op k) :.: +type YonedaEmbedding k =+ Postcompose (Hom k) (Op k) :.: (Postcompose (Swap k (Op k)) (Op k) :.: Tuple k (Op k)) -- | The Yoneda embedding functor, @C -> Set^(C^op)@.@@ -31,11 +30,11 @@ type Cod (Yoneda k f) = (->) type Yoneda k f :% a = Nat (Op k) (->) (k :-*: a) f Yoneda % Op ab = \n -> n . yonedaEmbedding % ab- - ++ -- | 'fromYoneda' and 'toYoneda' are together the isomophism from the Yoneda lemma.-fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Yoneda k f :~> f+fromYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) (Yoneda k f) f fromYoneda f = Nat Yoneda f (\(Op a) n -> (n ! Op a) a) -toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> f :~> Yoneda k f+toYoneda :: (Category k, Functor f, Dom f ~ Op k, Cod f ~ (->)) => f -> Nat (Op k) (->) f (Yoneda k f) toYoneda f = Nat f Yoneda (\(Op a) fa -> Nat (hom_X a) f (\_ h -> (f % Op h) fa))
data-category.cabal view
@@ -1,5 +1,5 @@ name: data-category-version: 0.6.1+version: 0.6.2 synopsis: Category theory description: Data-category is a collection of categories, and some categorical constructions on them.@@ -41,7 +41,6 @@ Data.Category.Monoidal, Data.Category.CartesianClosed, Data.Category.Yoneda,- Data.Category.Presheaf, Data.Category.Boolean, Data.Category.Fix, Data.Category.Kleisli,