Processing math: 100%

Library CT.Instance.Functor.FAlgebra

Require Import CT.Category.
Require Import CT.Functor.
Require Import CT.Instance.Functor.Endofunctor.

F-Algebras

(a.k.a. "an algebra over an endofunctor").

Given a category

$C$ and endofunctor

$F$ on

$C$ , an F-algebra over

$F$ is given by an object

$X \in$ ob

$C$ along with a morphism

$\alpha : F(X) \to X$ .

Here

$X$ is called the carrier of the algebra.

See nlab for more details.

Section FAlgebra.
  Context {C : Category}.
  Context {F : Endofunctor C}.

  Record FAlgebra :=
    { FA_ob : ob C;
      FA_alpha : mor C (F_ob F FA_ob) FA_ob
    }.
End FAlgebra.