Category theory


This module defines the functors to be used in the semantics of coalgebraic logics.
In addition to the usual laws of preservation of identity morphisms and preservation of composition, the missing function extentionality in Coq requires a third law, namely preservation of extentional equality.

Require Export functions misc.

Record functor : Type := {
  obj : TypeType;
  fmap : {X Y : Type}, (XY) → ((obj X) → (obj Y));
  id_law : (X : Type), fmap (@id X) id;
  comp_law : (X Y Z : Type)(f : XY)(g : YZ),
               fmap (g f) (fmap g) (fmap f);
  fmap_feq_law : (X Y : Type)(f1 f2 : XY),
                   f1 f2fmap 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.

Definition non_trivial_functor(T : functor) : Prop :=
  (Y : Type), non_empty_type Ynon_empty_type (obj T Y).

Lemma non_empty_coalg : (T : functor)(X : Type),
  non_trivial_functor T
  non_empty_type X
    (f : Xobj T X), True.

This is a simple example to see if the defintions can be used at all
Definition x_nat_functor : functor.