# Confused about hierarchies of functions

Hi

I’m starting to think for my purposes Coq functions are too powerful.

So I want some smaller but still powerful set of functions.

But I’m unsure of how to work with these nicely or hierarchies here.

I’m thinking I could start with functions on finite types somewhat like the pseudocode below and then expand it as needed with products and such.

``````Class Finite A := {
N: nat ;
to: A -> Fin.t N ;
from: Fin.t N -> A ;
to_from x: to (from x) = x ;
from_to x: from (to x) = x ;
}.
Inductive Obj :=
| Fin (T: Type) (T_Finite: Finite T)
.

Inductive Mor: Obj -> Obj -> Type :=
| id A: Mor A A
| compose {A B C}: Mor B C -> Mor A B -> Mor A C

| fin {A B C D}: (A -> B) -> Mor (Fin A C) (Fib B D)
.``````

I somehow doubt it would be easy to use though.
And I have some other ideas for encodings like

``````Definition Map {A B} (f: list (A * B)) :=
forall x, exists! y, In (x, y).``````

But I’m very confused about hierarchies of functions and not really sure what adds in more power and what is redundant.

For example what if I add

``````Class Denumerable A := {
to: A -> nat ;
from: nat -> A ;
to_from x: to (from x) = x ;
from_to x: from (to x) = x ;
}.``````

Or

``````Class Uncountable A := {
to: A -> nat -> bool ;
from: (nat -> bool) -> A ;
to_from x y: to (from x) y = x y ;
from_to x: from (to x) = x ;
}.``````

Most stuff just focuses on abstract things like computability and relative power not stuff like practically coding in the subset of countable types.