Library UniMath.CategoryTheory.Inductives.Lists

This file contains formalizations of lists. First over sets as the initial algebra of the list functor (List) and then more generally over any type defined as iterated products (list).
Written by: Anders Mörtberg, 2016

Lists as the colimit of a chain given by the list functor: F(X) = 1 + A * X

Section lists.

Variable A : HSET.

Local Open Scope cocont_functor_hset_scope.

F(X) = 1 + (A * X)
The type of lists of A's
Get recursion/iteration scheme:
     x : X           f : A × X -> X
  ------------------------------------
       foldr x f : List A -> X
Definition mk_listAlgebra (X : HSET) (x : pr1 X)
  (f : HSET(A × X)%set,X) : algebra_ob listFunctor.
Proof.
set (x' := λ (_ : unit), x).
apply (tpair _ X (sumofmaps x' f) : algebra_ob listFunctor).
Defined.

Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET(A × X)%set,X) :
  algebra_mor _ List_alg (mk_listAlgebra X x f).
Proof.
apply (InitialArrow listFunctor_Initial (mk_listAlgebra X x f)).
Defined.

Iteration/fold
Definition foldr (X : HSET) (x : pr1 X)
  (f : pr1 A pr1 X pr1 X) : List pr1 X.
Proof.
apply (foldr_map _ x (λ a, f (pr1 a) (pr2 a))).
Defined.

Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A X X) : foldr X x f nil = x.
Proof.
assert (F := maponpaths (λ x, BinCoproductIn1 _ (BinCoproductsHSET _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X x (λ a, f (pr1 a) (pr2 a))))).
apply (toforallpaths _ _ _ F tt).
Qed.

Lemma foldr_cons (X : hSet) (x : X) (f : pr1 A X X)
                 (a : pr1 A) (l : List) :
  foldr X x f (cons a l) = f a (foldr X x f l).
Proof.
assert (F := maponpaths (λ x, BinCoproductIn2 _ (BinCoproductsHSET _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X x (λ a, f (pr1 a) (pr2 a))))).
assert (Fal := toforallpaths _ _ _ F (a,,l)).
clear F.
unfold compose in Fal.
simpl in Fal.
apply Fal.
Opaque foldr_map.
Qed. Transparent foldr_map.

The induction principle for lists defined using foldr
Section list_induction.

Variables (P : List UU) (PhSet : l, isaset (P l)).
Variables (P0 : P nil)
          (Pc : a l, P l P (cons a l)).

Let P' : UU := l, P l.
Let P0' : P' := (nil,, P0).
Let Pc' : pr1 A P' P' :=
  λ (a : pr1 A) (p : P'), cons a (pr1 p),,Pc a (pr1 p) (pr2 p).

Definition P'HSET : HSET.
Proof.
apply (tpair _ P').
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
Defined.

This line is crucial for isalghom_pr1foldr to typecheck
Opaque is_omega_cocont_listFunctor.

Lemma isalghom_pr1foldr :
  is_algebra_mor _ List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Proof.
apply (BinCoproductArrow_eq_cor _ BinCoproductsHSET).
- apply funextfun; intro x; induction x.
  apply (maponpaths pr1 (foldr_nil P'HSET P0' Pc')).
- apply funextfun; intro x; destruct x as [a l].
  apply (maponpaths pr1 (foldr_cons P'HSET P0' Pc' a l)).
Qed.

Transparent is_omega_cocont_listFunctor.

Definition pr1foldr_algmor : algebra_mor _ List_alg List_alg :=
  tpair _ _ isalghom_pr1foldr.

Lemma pr1foldr_algmor_identity : identity _ = pr1foldr_algmor.
Proof.
now rewrite (@InitialEndo_is_identity _ listFunctor_Initial pr1foldr_algmor).
Qed.

The induction principle for lists
Lemma listInd l : P l.
Proof.
assert (H : pr1 (foldr P'HSET P0' Pc' l) = l).
  apply (toforallpaths _ _ _ (!pr1foldr_algmor_identity) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
Defined.

End list_induction.

Lemma listIndhProp (P : List hProp) :
  P nil ( a l, P l P (cons a l)) l, P l.
Proof.
intros Pnil Pcons.
apply listInd; try assumption.
intro l; apply isasetaprop, propproperty.
Defined.

Lemma listIndProp (P : List UU) (HP : l, isaprop (P l)) :
  P nil ( a l, P l P (cons a l)) l, P l.
Proof.
intros Pnil Pcons.
apply listInd; try assumption.
intro l; apply isasetaprop, HP.
Defined.

Local Open Scope nat_scope.

Local Notation "'A'" := (pr1 A).

Definition length : List nat := foldr natHSET 0 (λ _ (n : nat), 1 + n).

Definition map (f : A A) : List List :=
  foldr _ nil (λ (x : A) (xs : List), cons (f x) xs).

Lemma length_map (f : A A) : xs, length (map f xs) = length xs.
Proof.
apply listIndProp.
- intros l; apply isasetnat.
- now unfold map; rewrite foldr_nil.
- simpl; unfold map, length; simpl; intros a l Hl.
  now rewrite !foldr_cons, <- Hl.
Qed.

Definition concatenate : List List List :=
  λ l l', foldr _ l cons l'.

End lists.

Some examples of computations with lists over nat
Section nat_examples.

Definition cons_nat a l : List natHSET := cons natHSET a l.

Local Infix "::" := cons_nat.
Local Notation "[]" := (nil natHSET) (at level 0, format "[]").

Definition testlist : List natHSET := 5 :: 2 :: [].

Definition testlistS : List natHSET :=
  map natHSET S testlist.

Definition sum : List natHSET nat :=
  foldr natHSET natHSET 0 (λ x y, x + y).


Goal length _ (nil natHSET) = 0. reflexivity. Qed.
Goal length _ testlist = length _ testlistS. reflexivity. Qed.
Goal sum testlistS = sum testlist + length _ testlist. lazy. reflexivity. Qed.
Goal length _ (concatenate _ testlist testlistS) = length _ testlist + length _ testlistS. reflexivity. Qed.
Goal sum (concatenate _ testlist testlistS) = sum testlistS + sum testlist. reflexivity. Qed.

Goal ( l, length _ (2 :: l) = S (length _ l)).
simpl.
intro l.
try apply idpath. unfold length, cons_nat.
rewrite foldr_cons. cbn.
apply idpath.
Abort.







End nat_examples.

Equivalence with lists as iterated products

Section list.

Lemma isaset_list (A : HSET) : isaset (list (pr1 A)).
Proof.
apply isaset_total2; [apply isasetnat|].
intro n; induction n as [|n IHn]; simpl; [apply isasetunit|].
apply isaset_dirprod; [ apply setproperty | apply IHn ].
Qed.

Definition to_List (A : HSET) : list (pr1 A) List A.
Proof.
intros l.
destruct l as [n l].
induction n as [|n IHn].
+ exact (nil A).
+ apply (cons _ (pr1 l) (IHn (pr2 l))).
Defined.

Definition to_list (A : HSET) : List A list (pr1 A).
Proof.
apply (foldr A (list (pr1 A),,isaset_list A)).
× apply (0,,tt).
× intros a L; simpl in ×.
  apply (tpair _ (S (pr1 L)) (a,,pr2 L)).
Defined.

Lemma to_listK (A : HSET) : x : list (pr1 A), to_list A (to_List A x) = x.
Proof.
intro l; destruct l as [n l]; unfold to_list, to_List.
induction n as [|n IHn]; simpl.
- rewrite foldr_nil.
  now destruct l.
- rewrite foldr_cons; simpl.
  now rewrite IHn.
Qed.

Lemma to_ListK (A : HSET) : y : List A, to_List A (to_list A y) = y.
Proof.
apply listIndProp.
× intro l; apply setproperty.
× now unfold to_list; rewrite foldr_nil.
× unfold to_list, to_List; intros a l IH.
  rewrite foldr_cons; simpl.
  apply maponpaths, pathsinv0.
  eapply pathscomp0; [eapply pathsinv0, IH|]; simpl.
  now destruct foldr.
Qed.

Equivalence between list and List for A a set
Lemma weq_list (A : HSET) : list (pr1 A) List A.
Proof.
use tpair.
- apply to_List.
- use isweq_iso.
  + apply to_list.
  + apply to_listK.
  + apply to_ListK.
Defined.


Goal to_list _ testlist = 2,,5,,2,,tt. reflexivity. Qed.

End list.

Alternative version of lists using a more direct proof of omega-cocontinuity. This definition has slightly better computational properties.
Module AltList.

Section constprod_functor.

Variables (x : HSET).

Definition constprod_functor : functor HSET HSET :=
  BinProduct_of_functors HSET HSET BinProductsHSET (constant_functor HSET HSET x)
                                         (functor_identity HSET).

Lemma omega_cocontConstProdFunctor : is_omega_cocont constprod_functor.
Proof.
intros hF c L ccL HcL cc.
use tpair.
- transparent assert (HX : (cocone hF (hset_fun_space x HcL))).
  { use mk_cocone.
    × simpl; intro n; apply flip, (curry (Z := λ _,_)), (pr1 cc).
    × abstract (destruct cc as [f hf]; simpl; intros m n e;
                rewrite <- (hf m n e); destruct e; simpl;
                repeat (apply funextfun; intro); apply idpath).
  }
  use tpair.
  + simpl; apply uncurry, flip.
    apply (colimArrow (mk_ColimCocone _ _ _ ccL) (hset_fun_space x HcL)).
    apply HX.
  + cbn.
    destruct cc as [f hf]; simpl; intro n.
    apply funextfun; intro p.
    change p with (pr1 p,,pr2 p).
    assert (XR := colimArrowCommutes (mk_ColimCocone hF c L ccL) _ HX n).
    unfold flip, curry, colimIn in *; simpl in ×.
    now rewrite <- (toforallpaths _ _ _ (toforallpaths _ _ _ XR (pr2 p)) (pr1 p)).
- abstract (
  intro p; unfold uncurry; simpl; apply subtypeEquality; simpl;
  [ intro g; apply impred; intro t;
    use (let ff : HSET (x × dob hF t)%set,HcL := _ in _);
    [ simpl; apply (pr1 cc)
    | apply (@has_homsets_HSET _ HcL _ ff) ]
  | destruct p as [t p]; simpl;
    apply funextfun; intro xc; destruct xc as [x' c']; simpl;
    use (let g : HSETcolim (mk_ColimCocone hF c L ccL),
                                hset_fun_space x HcL := _ in _);
    [ simpl; apply flip, (curry (Z := λ _,_)), t
    | rewrite <- (colimArrowUnique _ _ _ g); [apply idpath | ];
      destruct cc as [f hf]; simpl in *;
      now intro n; simpl; rewrite <- (p n) ]
  ]).
Defined.

End constprod_functor.

Section constcoprod_functor.

Variables (C : precategory) (hsC : has_homsets C) (x : C) (PC : BinCoproducts C).

Definition constcoprod_functor : functor C C :=
  BinCoproduct_of_functors C C PC (constant_functor C C x) (functor_identity C).

Lemma omega_cocontConstCoprodFunctor : is_omega_cocont constcoprod_functor.
Proof.
intros hF c L ccL HcL cc.
use tpair.
- use tpair.
  + eapply BinCoproductArrow.
    × exact (BinCoproductIn1 _ (PC x (dob hF 0)) · pr1 cc 0).
    × use (let ccHcL : cocone hF HcL := _ in _).
      { use mk_cocone.
        - intros n; exact (BinCoproductIn2 _ (PC x (dob hF n)) · pr1 cc n).
        - abstract (
            intros m n e; destruct e; simpl;
            destruct cc as [f hf]; simpl in *; unfold BinCoproduct_of_functors_ob in *;
            rewrite <- (hf m _ (idpath _)), !assoc; apply cancel_postcomposition;
            now unfold BinCoproduct_of_functors_mor; rewrite BinCoproductOfArrowsIn2). }
      apply (pr1 (pr1 (ccL HcL ccHcL))).
  + abstract (
    destruct cc as [f hf]; simpl in *; unfold BinCoproduct_of_functors_ob in *;
    simpl; intro n; unfold BinCoproduct_of_functors_mor in *;
    rewrite precompWithBinCoproductArrow; apply pathsinv0, BinCoproductArrowUnique;
    [ rewrite id_left; induction n as [|n IHn]; [apply idpath|];
      now rewrite <- IHn, <- (hf n _ (idpath _)), assoc,
                  BinCoproductOfArrowsIn1, id_left
    | rewrite <- (hf n _ (idpath _)); destruct ccL as [t p]; destruct t as [t p0]; simpl in *;
      rewrite p0; apply maponpaths, hf]).
- abstract (
  destruct cc as [f hf]; simpl in *; unfold BinCoproduct_of_functors_ob in *;
  intro t; apply subtypeEquality; simpl;
  [ intro g; apply impred; intro; apply hsC
  | destruct t as [t p]; destruct ccL as [t0 p0]; unfold BinCoproduct_of_functors_mor in *; destruct t0 as [t0 p1]; simpl;
    apply BinCoproductArrowUnique;
    [ now rewrite <- (p 0), assoc, BinCoproductOfArrowsIn1, id_left
    | use (let temp : x0 : C c, HcL , v : nat,
         coconeIn L v · x0 = BinCoproductIn2 C (PC x (dob hF v)) · f v := _ in _);
         [ apply (tpair _ (BinCoproductIn2 C (PC x c) · t));
          now intro n; rewrite <- (p n), !assoc, BinCoproductOfArrowsIn2|];
      apply (maponpaths pr1 (p0 temp))]]).
Defined.

End constcoprod_functor.

Section lists.

Variable A : HSET.

Definition stream : functor HSET HSET := constprod_functor1 BinProductsHSET A.

Definition listFunctor : functor HSET HSET :=
  functor_composite stream (constcoprod_functor _ unitHSET BinCoproductsHSET).

Lemma omega_cocont_listFunctor : is_omega_cocont listFunctor.
Proof.
apply (is_omega_cocont_functor_composite has_homsets_HSET).
- apply omega_cocontConstProdFunctor.
- apply (omega_cocontConstCoprodFunctor _ has_homsets_HSET).
Defined.

Lemma listFunctor_Initial :
  Initial (precategory_FunctorAlg listFunctor has_homsets_HSET).
Proof.
apply (colimAlgInitial _ InitialHSET omega_cocont_listFunctor (ColimCoconeHSET _ _)).
Defined.

Definition List : HSET :=
  alg_carrier _ (InitialObject listFunctor_Initial).

Let List_mor : HSETlistFunctor List,List :=
  alg_map _ (InitialObject listFunctor_Initial).

Let List_alg : algebra_ob listFunctor :=
  InitialObject listFunctor_Initial.

Definition nil_map : HSETunitHSET,List.
Proof.
simpl; intro x.
use List_mor.
apply inl.
exact x.
Defined.

Definition nil : pr1 List := nil_map tt.

Definition cons_map : HSET(A × List)%set,List.
Proof.
intros xs.
use List_mor.
exact (inr xs).
Defined.

Definition cons : pr1 A × pr1 List pr1 List := cons_map.



Definition mk_listAlgebra (X : HSET) (x : pr1 X)
  (f : HSET(A × X)%set,X) : algebra_ob listFunctor.
Proof.
set (x' := λ (_ : unit), x).
apply (tpair _ X (sumofmaps x' f) : algebra_ob listFunctor).
Defined.

Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET(A × X)%set,X) :
  algebra_mor _ List_alg (mk_listAlgebra X x f).
Proof.
apply (InitialArrow listFunctor_Initial (mk_listAlgebra X x f)).
Defined.

Definition foldr (X : HSET) (x : pr1 X)
  (f : pr1 A × pr1 X pr1 X) : pr1 List pr1 X.
Proof.
apply (foldr_map _ x f).
Defined.

Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A × X X) : foldr X x f nil = x.
Proof.
assert (F := maponpaths (λ x, BinCoproductIn1 _ (BinCoproductsHSET _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F tt).
Qed.

Lemma foldr_cons (X : hSet) (x : X) (f : pr1 A × X X)
                 (a : pr1 A) (l : pr1 List) :
  foldr X x f (cons (a,,l)) = f (a,,foldr X x f l).
Proof.
assert (F := maponpaths (λ x, BinCoproductIn2 _ (BinCoproductsHSET _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F (a,,l)).
Qed.

Section list_induction.

Variables (P : pr1 List UU) (PhSet : l, isaset (P l)).
Variables (P0 : P nil)
          (Pc : (a : pr1 A) (l : pr1 List), P l P (cons (a,,l))).

Let P' : UU := l, P l.
Let P0' : P' := (nil,, P0).
Let Pc' : pr1 A × P' P' :=
  λ ap : pr1 A × P', cons (pr1 ap,, pr1 (pr2 ap)),,Pc (pr1 ap) (pr1 (pr2 ap)) (pr2 (pr2 ap)).

Definition P'HSET : HSET.
Proof.
apply (tpair _ P').
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
Defined.

Lemma isalghom_pr1foldr :
  is_algebra_mor _ List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Proof.
apply BinCoproductArrow_eq_cor.
- apply funextfun; intro x; destruct x; apply idpath.
- apply funextfun; intro x; destruct x as [a l].
  apply (maponpaths pr1 (foldr_cons P'HSET P0' Pc' a l)).
Qed.

Definition pr1foldr_algmor : algebra_mor _ List_alg List_alg :=
  tpair _ _ isalghom_pr1foldr.

Lemma pr1foldr_algmor_identity : identity _ = pr1foldr_algmor.
Proof.
now rewrite (@InitialEndo_is_identity _ listFunctor_Initial pr1foldr_algmor).
Qed.

Lemma listInd l : P l.
Proof.
assert (H : pr1 (foldr P'HSET P0' Pc' l) = l).
  apply (toforallpaths _ _ _ (!pr1foldr_algmor_identity) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
Defined.

End list_induction.

Lemma listIndProp (P : pr1 List UU) (HP : l, isaprop (P l)) :
  P nil ( a l, P l P (cons (a,, l))) l, P l.
Proof.
intros Pnil Pcons.
apply listInd; try assumption.
intro l; apply isasetaprop, HP.
Defined.

Definition natHSET : HSET.
Proof.
nat.
abstract (apply isasetnat).
Defined.

Definition length : pr1 List nat :=
  foldr natHSET 0 (λ x, S (pr2 x)).

Definition map (f : pr1 A pr1 A) : pr1 List pr1 List :=
  foldr _ nil (λ xxs : pr1 A × pr1 List, cons (f (pr1 xxs),, pr2 xxs)).

Lemma length_map (f : pr1 A pr1 A) : xs, length (map f xs) = length xs.
Proof.
apply listIndProp.
- intros l; apply isasetnat.
- apply idpath.
- simpl; unfold map, length; simpl; intros a l Hl.
  simpl.
  now rewrite !foldr_cons, <- Hl.
Qed.

End lists.

Section nat_examples.

Definition cons_nat a l : pr1 (List natHSET) := cons natHSET (a,,l).

Infix "::" := cons_nat.
Notation "[]" := (nil natHSET) (at level 0, format "[]").

Definition testlist : pr1 (List natHSET) := 5 :: 2 :: [].

Definition testlistS : pr1 (List natHSET) :=
  map natHSET S testlist.

Definition sum : pr1 (List natHSET) nat :=
  foldr natHSET natHSET 0 (λ xy, pr1 xy + pr2 xy).



Goal ( l, length _ (2 :: l) = S (length _ l)).
simpl.
intro l.
try apply idpath. unfold length, cons_nat.
rewrite foldr_cons. cbn.
apply idpath.
Abort.

End nat_examples.
End AltList.