1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
{-# language KindSignatures, PolyKinds, TypeFamilies,
NoImplicitPrelude, FlexibleContexts,
MultiParamTypeClasses, GADTs,
ConstraintKinds, FlexibleInstances, UndecidableInstances,
FunctionalDependencies, UndecidableSuperClasses #-}
module T11480a where
import Data.Kind (Type, Constraint)
import qualified Prelude
data Nat (c :: i -> i -> Type) (d :: j -> j -> Type) (f :: i -> j) (g :: i -> j)
class Functor p (Nat p (->)) p => Category (p :: i -> i -> Type)
class (Category dom, Category cod)
=> Functor (dom :: i -> i -> Type) (cod :: j -> j -> Type) (f :: i -> j)
| f -> dom cod
instance (Category c, Category d) => Category (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (Nat (Nat c d) (->)) (Nat c d)
instance (Category c, Category d) => Functor (Nat c d) (->) (Nat c d f)
instance Category (->)
instance Functor (->) (->) ((->) e)
instance Functor (->) (Nat (->) (->)) (->)
|
