Confused about hierarchies of functions

Miscellaneous
1

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.