data-category-0.7.1: Category theory

LicenseBSD-style (see the file LICENSE)
Maintainersjoerd@w3future.com
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Category.NNO

Description

 

Documentation

class HasTerminalObject k => HasNaturalNumberObject k where Source #

Associated Types

type NaturalNumberObject k :: * Source #

Instances
HasNaturalNumberObject ((->) :: Type -> Type -> Type) Source # 
Instance details

Defined in Data.Category.NNO

Associated Types

type NaturalNumberObject (->) :: Type Source #

data NatNum Source #

Constructors

Z 
S NatNum 

data PrimRec z s Source #

Constructors

PrimRec z s 
Instances
(Functor z, Functor s, Dom z ~ Unit, Cod z ~ Dom s, Dom s ~ Cod s) => Functor (PrimRec z s) Source # 
Instance details

Defined in Data.Category.NNO

Associated Types

type Dom (PrimRec z s) :: Type -> Type -> Type Source #

type Cod (PrimRec z s) :: Type -> Type -> Type Source #

type (PrimRec z s) :% a :: Type Source #

Methods

(%) :: PrimRec z s -> Dom (PrimRec z s) a b -> Cod (PrimRec z s) (PrimRec z s :% a) (PrimRec z s :% b) Source #

type Dom (PrimRec z s) Source # 
Instance details

Defined in Data.Category.NNO

type Dom (PrimRec z s) = Nat
type Cod (PrimRec z s) Source # 
Instance details

Defined in Data.Category.NNO

type Cod (PrimRec z s) = Cod z
type (PrimRec z s) :% (I1 ()) Source # 
Instance details

Defined in Data.Category.NNO

type (PrimRec z s) :% (I1 ()) = z :% ()
type (PrimRec z s) :% (I2 n) Source # 
Instance details

Defined in Data.Category.NNO

type (PrimRec z s) :% (I2 n) = s :% (PrimRec z s :% n)