Library Containers.Final_Coalgebra

Require Export Containers.Functor.

Record Coalgebra (F : Functor) := {
  coalg_carrier : Type;
  coalg_fun : coalg_carrier → F coalg_carrier
}.
Coercion coalg_carrier : Coalgebra >-> Sortclass.
Coercion coalg_fun : Coalgebra >-> Funclass.
Arguments coalg_carrier {_} _.
Arguments coalg_fun {_} _ / _.

Lemma Coalgebra_equiv_sigma {F : Functor} :
  {carrier : Type & carrier → F carrier} <~> Coalgebra F.
Proof.
  issig (@Build_Coalgebra F) (@coalg_carrier F) (@coalg_fun F).
Qed.

Record Coalgebra_Hom {F : Functor} (C1 C2 : Coalgebra F) := {
  coalg_hom_fun : C1 → C2;
  coalg_hom_path : C2 o coalg_hom_fun = map coalg_hom_fun o C1
}.
Arguments Build_Coalgebra_Hom {_} _ _ _ _.
Arguments coalg_hom_fun {_ _ _} _ / _.
Arguments coalg_hom_path {_ _ _} _.

Coercion coalg_hom_fun : Coalgebra_Hom >-> Funclass.

Lemma issig_Coalgebra_Hom {F} (C1 C2 : Coalgebra F) :
  {fun_ : C1 → C2 & C2 o fun_ = map fun_ o C1} <~>
  Coalgebra_Hom C1 C2.
Proof.
  issig (@Build_Coalgebra_Hom F C1 C2)
      (@coalg_hom_fun F C1 C2) (@coalg_hom_path F C1 C2).
Defined.

Definition is_final {F : Functor} (C : Coalgebra F) :=
  ∀ C', Contr (Coalgebra_Hom C' C).

Record Final_Coalgebra (F : Functor) := {
  final_coalg_coalgebra : Coalgebra F;
  final_coalg_final : is_final final_coalg_coalgebra
}.