lude

Haskell prelude alternative
git clone git://git.rr3.xyz/lude | git clone gits://git.rr3.xyz/lude
Log | Files | Refs | README | LICENSE

Hom.hs (1247B)

      1 module Lude.Algebra.Category.Hom (
      2     Hom (..),
      3 ) where
      4 
      5 import Lude.Algebra.Category.Core
      6 import Lude.Haskell
      7 
      8 -- NOTE: Ideally, we could use DerivingVia to implement (for all categories `p`
      9 -- and objects `a`) `Functorial` on `p a` and `p`, but DerivingVia doesn't
     10 -- really work with associated type families.
     11 
     12 --------------------------------------------------------------------------------
     13 
     14 -- | The Hom functor for a category
     15 --
     16 -- Most categories @p@ should implement `Functorial` directly, but @Hom p@ is
     17 -- available if they don't.
     18 type Hom :: forall i. Cat i -> Cat i
     19 newtype Hom p a b = MkHom {unHom :: p a b}
     20 
     21 instance (Categorical p) => Hom p a b `Witnesses` Mor (Hom p) a b where
     22     witness (MkHom f) = MkEvidence \\ witnessMor f
     23 
     24 instance (Categorical p) => Categorical (Hom p) where
     25     type Obj (Hom p) = Obj p
     26     identity = MkHom identity
     27     compose (MkHom f) (MkHom g) = MkHom (compose f g)
     28     witnessMor = witness
     29 
     30 instance (Categorical p) => Functorial (Hom p a) where
     31     type Dom (Hom p a) = Hom p
     32     type Cod (Hom p a) = Function
     33     map = compose
     34 
     35 instance (Categorical p) => Functorial (Hom p) where
     36     type Dom (Hom p) = Dual (Hom p)
     37     type Cod (Hom p) = Hom p ==> Function
     38     map (MkDual f) = Naturally (. f)