Library Containers.Initial_Algebra

Require Export Containers.Functor.

Record Algebra (F : Functor) := {
  alg_carrier : Type;
  alg_fun : F alg_carrier → alg_carrier
}.
Coercion alg_carrier : Algebra >-> Sortclass.
Coercion alg_fun : Algebra >-> Funclass.
Arguments alg_carrier {_} _.
Arguments alg_fun {_} _ / _.

Record Algebra_Morphism {F : Functor} (A1 A2 : Algebra F) := {
  alg_morph_fun : A1 → A2;
  alg_morph_path : A2 o map alg_morph_fun = alg_morph_fun o A1
}.
Arguments Build_Algebra_Morphism {_} _ _ _ _.
Arguments alg_morph_fun {_ _ _} _ / _.
Arguments alg_morph_path {_ _ _} _.

Coercion alg_morph_fun : Algebra_Morphism >-> Funclass.

Lemma path_Algebra_Morphism {F : Functor} {A1 A2 : Algebra F}
  (H1 H2 : Algebra_Morphism A1 A2) :
  ∀ p : alg_morph_fun H1 = alg_morph_fun H2,
    transport (fun h ⇒ alg_fun A2 o map h = h o alg_fun A1)
      p (alg_morph_path H1) =
    alg_morph_path H2 →
    H1 = H2.
Proof.
  destruct H1, H2; simpl.
  intros p1 p2.
  induction p1.
  induction p2.
  reflexivity.
Qed.

Definition alg_morphism_compose {F} {A1 A2 A3 : Algebra F}
    (H1 : Algebra_Morphism A2 A3) (H2 : Algebra_Morphism A1 A2) :
  Algebra_Morphism A1 A3.
Proof.
  destruct H1 as [h1 p1].
  destruct H2 as [h2 p2].
  serapply Build_Algebra_Morphism.
  - exact (h1 o h2).
  - exact (ap (fun f ⇒ A3 o f) (f_map_path_composition F h2 h1) @
          (ap (fun f ⇒ f o map h2) p1) @
          (ap (fun f ⇒ h1 o f) p2)).
Defined.
Notation "H1 'oH' H2" := (alg_morphism_compose H1 H2) (at level 60).

Definition alg_morphism_id {F} (A : Algebra F) :
  Algebra_Morphism A A.
Proof.
  serapply Build_Algebra_Morphism.
  - exact idmap.
  - exact (ap (fun f ⇒ A o f) (f_map_path_id F A)).
Defined.

Definition is_initial {F : Functor} (A : Algebra F) :=
  ∀ A', Contr (Algebra_Morphism A A').

Lemma initial_algebra_unique {F} (A1 A2 : Algebra F) :
  is_initial A1 → is_initial A2 → A1 <~> A2.
Proof.
  intros I1 I2.
  destruct (I1 A2) as [H12 U12].
  destruct (I2 A1) as [H21 U21].
  destruct (I1 A1) as [H11 U11].
  destruct (I2 A2) as [H22 U22].
  serapply equiv_adjointify.
  - exact H12.
  - exact H21.
  - pose (p1 := ap alg_morph_fun (U22 (H12 oH H21))).
    pose (p2 := ap alg_morph_fun (U22 (alg_morphism_id A2))).
    pose (p := p1^ @ p2).
    intros x.
    exact (ap10 p x).
  - pose (p1 := ap alg_morph_fun (U11 (H21 oH H12))).
    pose (p2 := ap alg_morph_fun (U11 (alg_morphism_id A1))).
    pose (p := p1^ @ p2).
    intros x.
    exact (ap10 p x).
Qed.

Definition is_inductive {F : Functor} (A : Algebra F) :=
∀ P, (∀ IH : F {a : A & P a}, P (A (map pr1 IH))) → ∀ a, P a.

Definition is_initial' {F : Functor} (A : Algebra F) :=
  ∀ A', ∃ H : Algebra_Morphism A A', ∀ H',
    alg_morph_fun H = alg_morph_fun H'.

Goal ∀ F (A : Algebra F), is_initial' A → is_inductive A.
Proof.
  intros F A init.
  unfold is_inductive.
  intros P step a.
  set (alg := Build_Algebra F
                            {a : A & P a}
                            (fun IH ⇒ (A (map pr1 IH); step IH))).
  destruct (init alg) as [H unique].
  set (H' := Build_Algebra_Morphism alg A pr1 idpath).
  set (H'' := H' oH H).
  assert (p : alg_morph_fun H'' = alg_morphism_id A). {
    rewrite <- ((init A).2 H'').
    rewrite <- ((init A).2 (alg_morphism_id A)).
    reflexivity.
  }
  exact (transport _ (ap10 p a) (alg_morph_fun H a).2).
Qed.