Category theory

Functors

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 : 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.

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

Definition x_nat_functor : functor.