{-# OPTIONS --without-K --safe #-}
module Categories.Functor.Coalgebra where

-- Co-algebras of a Functor
open import Level
open import Function using (_$_)

open import Categories.Category using (Category)
open import Categories.Functor using (Functor; Endofunctor)

private
  variable
    o  e : Level

module _ {C : Category o  e} where

  F-Coalgebra-on : Endofunctor C  C .Category.Obj  Set 
  F-Coalgebra-on F A = A  F₀ A where open Category C; open Functor F

  record F-Coalgebra (F : Endofunctor C) : Set (o  ) where
    open Category C
    field
      A : Obj
      α : F-Coalgebra-on F A

  to-Coalgebra : {A : Category.Obj C}  {F : Endofunctor C}  (F-Coalgebra-on F A)  (F-Coalgebra F)
  to-Coalgebra {A = A} α = record {A = A; α = α}

  open F-Coalgebra

  -- Given a F-Coalgebra F, one can apply F to it to obtain an new 'iterated' F-Coalgebra
  iterate : {F : Endofunctor C}  F-Coalgebra F  F-Coalgebra F
  iterate {F = F} F-alg = record { A = Functor.F₀ F $ A F-alg ; α = Functor.F₁ F $ α F-alg }

  module _ {F : Endofunctor C} (X Y : F-Coalgebra F) where
    open Category C using (_⇒_; _∘_; _≈_)
    open Functor F using (F₁)
    private
      module X = F-Coalgebra X
      module Y = F-Coalgebra Y
    is-F-Coalgebra-Morphism : (X.A  Y.A)  (Set e)
    is-F-Coalgebra-Morphism f = Y.α  f  F₁ f  X.α

    record F-Coalgebra-Morphism : Set (  e) where
      field
        f : X.A  Y.A
        commutes : is-F-Coalgebra-Morphism f