# Category theory

## Functors

Require Export functions misc.

Record functor : Type := {

obj : Type → Type;

fmap : ∀{X Y : Type}, (X → Y) → ((obj X) → (obj Y));

id_law : ∀(X : Type), fmap (@id X) ≡ id;

comp_law : ∀(X Y Z : Type)(f : X → Y)(g : Y → Z),

fmap (g ∘ f) ≡ (fmap g) ∘ (fmap f);

fmap_feq_law : ∀(X Y : Type)(f1 f2 : X → Y),

f1 ≡ f2 → fmap f1 ≡ fmap f2

}.

With respect to non-trivial functors, the paper says

TX ≠ \emptyset for some set X;

it follows that TY = \emptyset only if Y = \emptyset
Firstly, I don't know how the second point follows from the first.
Moreover, a definition like

Definition non_trivial_functor(T : functor) : Prop :=

∀(Y : Type), empty_type (obj T Y) → empty_type Y.

is not useful, because from it I cannot derive the existence of an
element in obj T Y from an element in Y. I therefore use the
contrapositive of this definition.

TX ≠ \emptyset for some set X;

it follows that TY = \emptyset only if Y = \emptyset

Definition non_trivial_functor(T : functor) : Prop :=

∀(Y : Type), empty_type (obj T Y) → empty_type Y.

Definition non_trivial_functor(T : functor) : Prop :=

∀(Y : Type), non_empty_type Y → non_empty_type (obj T Y).

Lemma non_empty_coalg : ∀(T : functor)(X : Type),

non_trivial_functor T →

non_empty_type X →

∃(f : X → obj T X), True.

This is a simple example to see if the defintions can be used at
all