SubHask.Category.Trans.Bijective

Provides transformer categories for injective, surjective, and bijective functions.

TODO: Add Epic, Monic, and Iso categories.

Documentation

class Concrete cat => Injective cat

Injective (one-to-one) functions map every input to a unique output. See wikipedia for more detail.

Instances

Concrete cat => Injective (BijectiveT * * cat)

Concrete cat => Injective (InjectiveT * * cat)

data InjectiveT cat a b

Instances

Category k cat => Category k (InjectiveT k k cat)

Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (InjectiveT k k b) c

(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (InjectiveT k k subcat) cat

Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (InjectiveT k k a) b c

Concrete cat => Injective (InjectiveT * * cat)

type ValidCategory k (InjectiveT k k cat) a = ValidCategory k cat a

unsafeProveInjective :: Concrete cat => cat a b -> InjectiveT cat a b

class Concrete cat => Surjective cat

Surjective (onto) functions can take on every value in the range. See wikipedia for more detail.

Instances

Concrete cat => Surjective (BijectiveT * * cat)

Concrete cat => Surjective (SurjectiveT * * cat)

data SurjectiveT cat a b

Instances

Category k cat => Category k (SurjectiveT k k cat)

Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (SurjectiveT k k b) c

(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (SurjectiveT k k subcat) cat

Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (SurjectiveT k k a) b c

Concrete cat => Surjective (SurjectiveT * * cat)

type ValidCategory k (SurjectiveT k k cat) a = ValidCategory k cat a

unsafeProveSurjective :: Concrete cat => cat a b -> SurjectiveT cat a b

class (Injective cat, Surjective cat) => Bijective cat

Bijective functions are both injective and surjective. See wikipedia for more detail.

Instances

Concrete cat => Bijective (BijectiveT * * cat)

data BijectiveT cat a b

Instances

Category k cat => Category k (BijectiveT k k cat)

Sup (k -> k1 -> *) b a c => Sup (k -> k -> *) a (BijectiveT k k b) c

(<:) (k -> k1 -> *) subcat cat => (<:) (k -> k -> *) (BijectiveT k k subcat) cat

Sup (k -> k1 -> *) a b c => Sup (k -> k -> *) (BijectiveT k k a) b c

Concrete cat => Bijective (BijectiveT * * cat)

Concrete cat => Surjective (BijectiveT * * cat)

Concrete cat => Injective (BijectiveT * * cat)

type ValidCategory k (BijectiveT k k cat) a = ValidCategory k cat a

proveBijective :: (Injective cat, Surjective cat) => cat a b -> BijectiveT cat a b

unsafeProveBijective :: Concrete cat => cat a b -> BijectiveT cat a b