Library UniMath.CategoryTheory.Chains.Adamek

Adámek's theorem

The main result is Adámek's theorem for constructing initial algebras of omega-cocontinuous functors (colimAlgIsInitial) which is used to construct inductive types.
Written by: Anders Mörtberg and Benedikt Ahrens, 2015-2016

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.

Require Import UniMath.CategoryTheory.Chains.Chains.

Local Open Scope cat.

Adámek's theorem for constructing initial algebras of omega-cocontinuous functors

This section proves that (L,α : F L -> L) is the initial algebra where L is the colimit of the initial chain: 
         !          F !           F^2 !
     0 -----> F 0 ------> F^2 0 --------> F^3 0 ---> ...
This result is also known as Adámek's theorem
https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunctorAdameksTheorem Adámek, Jiří. "Free algebras and automata realizations in the language of categories." Commentationes Mathematicae Universitatis Carolinae 015.4 (1974): 589-602.
Section colim_initial_algebra.

Context {C : category} (InitC : Initial C).

Context {F : functor C C} (HF : is_omega_cocont F).

Let Fchain : chain C := initChain InitC F.

Variable (CC : ColimCocone Fchain).

Let L : C := colim CC.
Let FFchain : chain C := mapchain F Fchain.
Let Fa : cocone FFchain (F L) := mapcocone F _ (colimCocone CC).
Let FHC' : isColimCocone FFchain (F L) Fa :=
  HF Fchain L (colimCocone CC) (isColimCocone_from_ColimCocone CC).
Let FHC : ColimCocone FFchain := make_ColimCocone _ _ _ FHC'.

Local Definition shiftCocone : cocone FFchain L.
Show proof.
use make_cocone.
- intro n; apply (coconeIn (colimCocone CC) (S n)).
- abstract (intros m n e; destruct e ;
            apply (coconeInCommutes (colimCocone CC) (S m) _ (idpath _))).

Local Definition unshiftCocone (x : C) (cc : cocone FFchain x) : cocone Fchain x.
Show proof.
use make_cocone.
- simpl; intro n.
  induction n as [|n]; simpl.
  + apply InitialArrow.
  + apply (coconeIn cc _).
- abstract (simpl; intros m n e; destruct e;
            destruct m as [|m]; [ apply InitialArrowUnique
                                | apply (coconeInCommutes cc m _ (idpath _))]).

Local Definition shiftIsColimCocone : isColimCocone FFchain L shiftCocone.
Show proof.
intros x cc; simpl.
use tpair.
+ use tpair.
  * apply colimArrow, (unshiftCocone _ cc).
  * abstract (intro n; apply (colimArrowCommutes CC x (unshiftCocone x cc) (S n))).
+ abstract (intros p; apply subtypePath;
             [ intro f; apply impred; intro; apply homset_property
             | apply colimArrowUnique; intro n;
               destruct n as [|n]; [ apply InitialArrowUnique | apply (pr2 p) ]]).

Local Definition shiftColimCocone : ColimCocone FFchain :=
  make_ColimCocone FFchain L shiftCocone shiftIsColimCocone.

Definition colim_algebra_mor : C⟦F L,L⟧ := colimArrow FHC L shiftCocone.

Local Definition is_z_iso_colim_algebra_mor : is_z_isomorphism colim_algebra_mor :=
  isColim_is_z_iso _ FHC _ _ shiftIsColimCocone.

Let α : z_iso (F L) L := make_z_iso' _ is_z_iso_colim_algebra_mor.
Let α_inv : z_iso L (F L) := z_iso_inv_from_z_iso α.
Let α_alg : algebra_ob F := tpair (λ X : C, C ⟦ F X, X ⟧) L α.

Lemma unfold_inv_from_z_iso_α :
  inv_from_z_iso α = colimArrow shiftColimCocone _ (colimCocone FHC).
Show proof.
apply idpath.

Given an algebra: 
          a
   F A ------> A
we now define an algebra morphism ad: 
          α
   F L ------> L
    |          |
    |          | ad
    |          |
    V     a    V
   F A ------> A
Section algebra_mor.

Variable (Aa : algebra_ob F).

Local Notation A := (alg_carrier _ Aa).
Local Notation a := (alg_map _ Aa).

Local Definition cocone_over_alg (n : nat) : C ⟦ dob Fchain n, A ⟧.
Show proof.
induction n as [|n Fn]; simpl.
- now apply InitialArrow.
- now apply (# F Fn · a).

Local Notation an := cocone_over_alg.

Arguments dmor : simpl never.

Lemma isCoconeOverAlg n Sn (e : edge n Sn) : dmor Fchain e · an Sn = an n.
Show proof.
destruct e.
induction n as [|n IHn].
- now apply InitialArrowUnique.
- simpl; rewrite assoc.
  apply cancel_postcomposition, pathsinv0.
  eapply pathscomp0; [|simpl; apply functor_comp].
  now apply maponpaths, pathsinv0, IHn.

Local Definition : C⟦L,A⟧.
Show proof.
apply colimArrow.
use make_cocone.
- apply cocone_over_alg.
- red; apply isCoconeOverAlg.

Lemma ad_is_algebra_mor : is_algebra_mor _ α_alg Aa ad.
Show proof.
apply pathsinv0, z_iso_inv_to_left, colimArrowUnique; simpl; intro n.
destruct n as [|n].
- now apply InitialArrowUnique.
- rewrite assoc, unfold_inv_from_z_iso_α.
  eapply pathscomp0;
    [apply cancel_postcomposition, (colimArrowCommutes shiftColimCocone)|].
  simpl; rewrite assoc, <- functor_comp.
  apply cancel_postcomposition, maponpaths, (colimArrowCommutes CC).

Local Definition ad_mor : algebra_mor F α_alg Aa := tpair _ _ ad_is_algebra_mor.

End algebra_mor.

Lemma colimAlgIsInitial_subproof (Aa : category_FunctorAlg F)
        (Fa' : algebra_mor F α_alg Aa) : Fa' = ad_mor Aa.
Show proof.
apply algebra_mor_eq; simpl.
apply colimArrowUnique; simpl; intro n.
destruct Fa' as [f hf]; simpl.
unfold is_algebra_mor in hf; simpl in hf.
induction n as [|n IHn]; simpl.
- now apply InitialArrowUnique.
- rewrite <- IHn, functor_comp, <- assoc.
  eapply pathscomp0; [| eapply maponpaths; apply hf].
  rewrite assoc.
  apply cancel_postcomposition, pathsinv0, (z_iso_inv_to_right _ _ _ _ α).
  rewrite unfold_inv_from_z_iso_α; apply pathsinv0.
  now eapply pathscomp0; [apply (colimArrowCommutes shiftColimCocone)|].

Lemma colimAlgIsInitial : isInitial (category_FunctorAlg F) α_alg.
Show proof.
apply make_isInitial; intros Aa.
exists (ad_mor Aa).
apply colimAlgIsInitial_subproof.

Definition colimAlgInitial : Initial (category_FunctorAlg F) :=
  make_Initial _ colimAlgIsInitial.

End colim_initial_algebra.