Library UniMath.CategoryTheory.Inductives.Lists
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Combinatorics.Lists.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.Chains.All.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Local Open Scope cat.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.Combinatorics.Lists.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.Chains.All.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Local Open Scope cat.
F(X) = 1 + (A * X)
Definition L_A : omega_cocont_functor HSET HSET := '1 + 'A * Id.
Let listFunctor : functor HSET HSET := pr1 L_A.
Let is_omega_cocont_listFunctor : is_omega_cocont listFunctor := pr2 L_A.
Lemma listFunctor_Initial :
Initial (category_FunctorAlg listFunctor).
Show proof.
Let listFunctor : functor HSET HSET := pr1 L_A.
Let is_omega_cocont_listFunctor : is_omega_cocont listFunctor := pr2 L_A.
Lemma listFunctor_Initial :
Initial (category_FunctorAlg listFunctor).
Show proof.
The type of lists of A's
Definition μL_A : HSET :=
alg_carrier _ (InitialObject listFunctor_Initial).
Definition List : UU := pr1 μL_A.
Let List_mor : HSET⟦listFunctor μL_A,μL_A⟧ :=
alg_map _ (InitialObject listFunctor_Initial).
Let List_alg : algebra_ob listFunctor :=
InitialObject listFunctor_Initial.
Definition nil_map : HSET⟦unitHSET,μL_A⟧ :=
BinCoproductIn1 (BinCoproductsHSET _ _) · List_mor.
Definition nil : List := nil_map tt.
Definition cons_map : HSET⟦(A × μL_A)%set,μL_A⟧ :=
BinCoproductIn2 (BinCoproductsHSET _ _) · List_mor.
Definition cons : pr1 A → List -> List := λ a l, cons_map (a,,l).
alg_carrier _ (InitialObject listFunctor_Initial).
Definition List : UU := pr1 μL_A.
Let List_mor : HSET⟦listFunctor μL_A,μL_A⟧ :=
alg_map _ (InitialObject listFunctor_Initial).
Let List_alg : algebra_ob listFunctor :=
InitialObject listFunctor_Initial.
Definition nil_map : HSET⟦unitHSET,μL_A⟧ :=
BinCoproductIn1 (BinCoproductsHSET _ _) · List_mor.
Definition nil : List := nil_map tt.
Definition cons_map : HSET⟦(A × μL_A)%set,μL_A⟧ :=
BinCoproductIn2 (BinCoproductsHSET _ _) · List_mor.
Definition cons : pr1 A → List -> List := λ a l, cons_map (a,,l).
Get recursion/iteration scheme:
x : X f : A × X -> X
------------------------------------
foldr x f : List A -> X
Definition make_listAlgebra (X : HSET) (x : pr1 X)
(f : HSET⟦(A × X)%set,X⟧) : algebra_ob listFunctor.
Show proof.
Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET⟦(A × X)%set,X⟧) :
algebra_mor _ List_alg (make_listAlgebra X x f).
Show proof.
(f : HSET⟦(A × X)%set,X⟧) : algebra_ob listFunctor.
Show proof.
Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET⟦(A × X)%set,X⟧) :
algebra_mor _ List_alg (make_listAlgebra X x f).
Show proof.
Iteration/fold
Definition foldr (X : HSET) (x : pr1 X)
(f : pr1 A → pr1 X → pr1 X) : List → pr1 X.
Show proof.
Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A → X -> X) : foldr X x f nil = x.
Show proof.
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).
Show proof.
(f : pr1 A → pr1 X → pr1 X) : List → pr1 X.
Show proof.
Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A → X -> X) : foldr X x f nil = x.
Show 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).
(algebra_mor_commutes _ _ _ (foldr_map X x (λ a, f (pr1 a) (pr2 a))))).
apply (toforallpaths _ _ _ F tt).
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).
Show 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.
Transparent foldr_map.(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.
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.
Show proof.
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.
Show proof.
apply (tpair _ P').
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
This line is crucial for isalghom_pr1foldr to typecheck
Opaque is_omega_cocont_listFunctor.
Lemma isalghom_pr1foldr :
is_algebra_mor listFunctor List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Show proof.
Definition pr1foldr_algmor : algebra_mor listFunctor List_alg List_alg.
Show proof.
Transparent is_omega_cocont_listFunctor.
Lemma pr1foldr_algmor_identity : identity List_alg = pr1foldr_algmor.
Show proof.
Lemma isalghom_pr1foldr :
is_algebra_mor listFunctor List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Show 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)).
- 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)).
Definition pr1foldr_algmor : algebra_mor listFunctor List_alg List_alg.
Show proof.
Transparent is_omega_cocont_listFunctor.
Lemma pr1foldr_algmor_identity : identity List_alg = pr1foldr_algmor.
Show proof.
The induction principle for lists
Lemma listInd l : P l.
Show proof.
End list_induction.
Lemma listIndhProp (P : List → hProp) :
P nil → (∏ a l, P l → P (cons a l)) → ∏ l, P l.
Show proof.
Lemma listIndProp (P : List → UU) (HP : ∏ l, isaprop (P l)) :
P nil → (∏ a l, P l → P (cons a l)) → ∏ l, P l.
Show proof.
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.
Show proof.
Definition concatenate : List -> List -> List :=
λ l l', foldr _ l cons l'.
End lists.
Show proof.
assert (H : pr1 (foldr P'HSET P0' Pc' l) = l).
apply (toforallpaths _ _ _ (maponpaths pr1 (!pr1foldr_algmor_identity)) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
apply (toforallpaths _ _ _ (maponpaths pr1 (!pr1foldr_algmor_identity)) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
End list_induction.
Lemma listIndhProp (P : List → hProp) :
P nil → (∏ a l, P l → P (cons a l)) → ∏ l, P l.
Show proof.
Lemma listIndProp (P : List → UU) (HP : ∏ l, isaprop (P l)) :
P nil → (∏ a l, P l → P (cons a l)) → ∏ l, P l.
Show proof.
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.
Show 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.
- intros l; apply isasetnat.
- now unfold map; rewrite foldr_nil.
- simpl; unfold map, length; simpl; intros a l Hl.
now rewrite !foldr_cons, <- Hl.
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.
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.
Section list.
Lemma isaset_list (A : HSET) : isaset (list (pr1 A)).
Show proof.
Definition to_List (A : HSET) : list (pr1 A) -> List A.
Show proof.
Definition to_list (A : HSET) : List A -> list (pr1 A).
Show proof.
Lemma to_listK (A : HSET) : ∏ x : list (pr1 A), to_list A (to_List A x) = x.
Show proof.
Lemma to_ListK (A : HSET) : ∏ y : List A, to_List A (to_list A y) = y.
Show proof.
Lemma isaset_list (A : HSET) : isaset (list (pr1 A)).
Show proof.
apply isaset_total2; [apply isasetnat|].
intro n; induction n as [|n IHn]; simpl; [apply isasetunit|].
apply isaset_dirprod; [ apply setproperty | apply IHn ].
intro n; induction n as [|n IHn]; simpl; [apply isasetunit|].
apply isaset_dirprod; [ apply setproperty | apply IHn ].
Definition to_List (A : HSET) : list (pr1 A) -> List A.
Show proof.
intros l.
destruct l as [n l].
induction n as [|n IHn].
+ exact (nil A).
+ apply (cons _ (pr1 l) (IHn (pr2 l))).
destruct l as [n l].
induction n as [|n IHn].
+ exact (nil A).
+ apply (cons _ (pr1 l) (IHn (pr2 l))).
Definition to_list (A : HSET) : List A -> list (pr1 A).
Show 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)).
* apply (0,,tt).
* intros a L; simpl in *.
apply (tpair _ (S (pr1 L)) (a,,pr2 L)).
Lemma to_listK (A : HSET) : ∏ x : list (pr1 A), to_list A (to_List A x) = x.
Show 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.
induction n as [|n IHn]; simpl.
- rewrite foldr_nil.
now destruct l.
- rewrite foldr_cons; simpl.
now rewrite IHn.
Lemma to_ListK (A : HSET) : ∏ y : List A, to_List A (to_list A y) = y.
Show 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.
* 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.
Equivalence between list and List for A a set
Lemma weq_list (A : HSET) : list (pr1 A) ≃ List A.
Show proof.
Goal to_list _ testlist = 2,,5,,2,,tt. reflexivity. Qed.
End list.
Show proof.
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.
Show proof.
End constprod_functor.
Section constcoprod_functor.
Variables (C : category) (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.
Show proof.
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.
Show proof.
Lemma listFunctor_Initial :
Initial (category_FunctorAlg listFunctor).
Show proof.
Definition List : HSET :=
alg_carrier _ (InitialObject listFunctor_Initial).
Let List_mor : HSET⟦listFunctor List,List⟧ :=
alg_map _ (InitialObject listFunctor_Initial).
Let List_alg : algebra_ob listFunctor :=
InitialObject listFunctor_Initial.
Definition nil_map : HSET⟦unitHSET,List⟧.
Show proof.
Definition nil : pr1 List := nil_map tt.
Definition cons_map : HSET⟦(A × List)%set,List⟧.
Show proof.
Definition cons : pr1 A × pr1 List -> pr1 List := cons_map.
Definition make_listAlgebra (X : HSET) (x : pr1 X)
(f : HSET⟦(A × X)%set,X⟧) : algebra_ob listFunctor.
Show proof.
Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET⟦(A × X)%set,X⟧) :
algebra_mor _ List_alg (make_listAlgebra X x f).
Show proof.
Definition foldr (X : HSET) (x : pr1 X)
(f : pr1 A × pr1 X -> pr1 X) : pr1 List -> pr1 X.
Show proof.
Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A × X -> X) : foldr X x f nil = x.
Show proof.
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).
Show proof.
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.
Show proof.
Lemma isalghom_pr1foldr :
is_algebra_mor _ List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Show proof.
Definition pr1foldr_algmor : algebra_mor _ List_alg List_alg :=
tpair _ _ isalghom_pr1foldr.
Lemma pr1foldr_algmor_identity : identity _ = pr1foldr_algmor.
Show proof.
Lemma listInd l : P l.
Show proof.
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.
Show proof.
Definition natHSET : HSET.
Show proof.
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.
Show proof.
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.
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.
Show proof.
intros hF c L ccL HcL cc.
use tpair.
- transparent assert (HX : (cocone hF (funset x HcL))).
{ use make_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 (make_ColimCocone _ _ _ ccL) (funset 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 (make_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 subtypePath; 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 : HSET⟦colim (make_ColimCocone hF c L ccL),
funset x HcL⟧ := _ in _);
[ simpl; apply flip, (curry (Z := λ _,_)), t
| rewrite <- (colimArrowUnique _ _ _ g); [apply idpath | ];
destruct cc as [f hf]; unfold is_cocone_mor in p; simpl in *;
now intro n; simpl; rewrite <- (p n) ]
]).
use tpair.
- transparent assert (HX : (cocone hF (funset x HcL))).
{ use make_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 (make_ColimCocone _ _ _ ccL) (funset 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 (make_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 subtypePath; 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 : HSET⟦colim (make_ColimCocone hF c L ccL),
funset x HcL⟧ := _ in _);
[ simpl; apply flip, (curry (Z := λ _,_)), t
| rewrite <- (colimArrowUnique _ _ _ g); [apply idpath | ];
destruct cc as [f hf]; unfold is_cocone_mor in p; simpl in *;
now intro n; simpl; rewrite <- (p n) ]
]).
End constprod_functor.
Section constcoprod_functor.
Variables (C : category) (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.
Show 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 make_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 *;
rewrite <- (hf m _ (idpath _)), !assoc; apply cancel_postcomposition;
unfold constcoprod_functor; cbn;
apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2|]; apply idpath). }
apply (pr1 (pr1 (ccL HcL ccHcL))).
+ abstract (
destruct cc as [f hf]; simpl in *;
simpl; intro n; unfold constcoprod_functor; cbn;
etrans; [apply precompWithBinCoproductArrow |]; apply pathsinv0, BinCoproductArrowUnique; red in hf;
[ rewrite id_left; induction n as [|n IHn]; [apply idpath|];
etrans; [| apply IHn]; unfold constant_functor; simpl; rewrite <- (hf n _ (idpath _)), assoc;
unfold constant_functor; simpl; apply pathsinv0;
etrans; [apply cancel_postcomposition; apply BinCoproductOfArrowsIn1 |]; now rewrite id_left
| rewrite <- (hf n _ (idpath _)); destruct ccL as [t p]; destruct t as [t p0]; simpl in *;
rewrite p0; simpl; now apply maponpaths, hf]).
- abstract (
destruct cc as [f hf]; simpl in *;
intro t; apply subtypePath; simpl;
[ intro g; apply impred; intro; apply C
| destruct t as [t p]; destruct ccL as [t0 p0]; unfold is_cocone_mor in *;
unfold constcoprod_functor; destruct t0 as [t0 p1]; simpl;
apply BinCoproductArrowUnique;
[ unfold coconeIn in p; simpl in p;
rewrite <- (p 0), assoc;
apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn1 |]; apply id_left
| use (let temp : ∑ x0 : C ⟦ c, HcL ⟧, ∏ v : nat,
coconeIn L v · x0 = BinCoproductIn2 (PC x (dob hF v)) · f v := _ in _);
[ apply (tpair _ (BinCoproductIn2 (PC x c) · t));
intro n; unfold coconeIn in p; simpl in p; rewrite <- (p n), !assoc;
apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2 |];
apply idpath|];
apply (maponpaths pr1 (p0 temp))]]).
use tpair.
- use tpair.
+ eapply BinCoproductArrow.
* exact (BinCoproductIn1 (PC x (dob hF 0)) · pr1 cc 0).
* use (let ccHcL : cocone hF HcL := _ in _).
{ use make_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 *;
rewrite <- (hf m _ (idpath _)), !assoc; apply cancel_postcomposition;
unfold constcoprod_functor; cbn;
apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2|]; apply idpath). }
apply (pr1 (pr1 (ccL HcL ccHcL))).
+ abstract (
destruct cc as [f hf]; simpl in *;
simpl; intro n; unfold constcoprod_functor; cbn;
etrans; [apply precompWithBinCoproductArrow |]; apply pathsinv0, BinCoproductArrowUnique; red in hf;
[ rewrite id_left; induction n as [|n IHn]; [apply idpath|];
etrans; [| apply IHn]; unfold constant_functor; simpl; rewrite <- (hf n _ (idpath _)), assoc;
unfold constant_functor; simpl; apply pathsinv0;
etrans; [apply cancel_postcomposition; apply BinCoproductOfArrowsIn1 |]; now rewrite id_left
| rewrite <- (hf n _ (idpath _)); destruct ccL as [t p]; destruct t as [t p0]; simpl in *;
rewrite p0; simpl; now apply maponpaths, hf]).
- abstract (
destruct cc as [f hf]; simpl in *;
intro t; apply subtypePath; simpl;
[ intro g; apply impred; intro; apply C
| destruct t as [t p]; destruct ccL as [t0 p0]; unfold is_cocone_mor in *;
unfold constcoprod_functor; destruct t0 as [t0 p1]; simpl;
apply BinCoproductArrowUnique;
[ unfold coconeIn in p; simpl in p;
rewrite <- (p 0), assoc;
apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn1 |]; apply id_left
| use (let temp : ∑ x0 : C ⟦ c, HcL ⟧, ∏ v : nat,
coconeIn L v · x0 = BinCoproductIn2 (PC x (dob hF v)) · f v := _ in _);
[ apply (tpair _ (BinCoproductIn2 (PC x c) · t));
intro n; unfold coconeIn in p; simpl in p; rewrite <- (p n), !assoc;
apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2 |];
apply idpath|];
apply (maponpaths pr1 (p0 temp))]]).
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.
Show proof.
apply (is_omega_cocont_functor_composite).
- apply omega_cocontConstProdFunctor.
- apply (omega_cocontConstCoprodFunctor _).
- apply omega_cocontConstProdFunctor.
- apply (omega_cocontConstCoprodFunctor _).
Lemma listFunctor_Initial :
Initial (category_FunctorAlg listFunctor).
Show proof.
Definition List : HSET :=
alg_carrier _ (InitialObject listFunctor_Initial).
Let List_mor : HSET⟦listFunctor List,List⟧ :=
alg_map _ (InitialObject listFunctor_Initial).
Let List_alg : algebra_ob listFunctor :=
InitialObject listFunctor_Initial.
Definition nil_map : HSET⟦unitHSET,List⟧.
Show proof.
Definition nil : pr1 List := nil_map tt.
Definition cons_map : HSET⟦(A × List)%set,List⟧.
Show proof.
Definition cons : pr1 A × pr1 List -> pr1 List := cons_map.
Definition make_listAlgebra (X : HSET) (x : pr1 X)
(f : HSET⟦(A × X)%set,X⟧) : algebra_ob listFunctor.
Show proof.
Definition foldr_map (X : HSET) (x : pr1 X) (f : HSET⟦(A × X)%set,X⟧) :
algebra_mor _ List_alg (make_listAlgebra X x f).
Show proof.
Definition foldr (X : HSET) (x : pr1 X)
(f : pr1 A × pr1 X -> pr1 X) : pr1 List -> pr1 X.
Show proof.
Lemma foldr_nil (X : hSet) (x : X) (f : pr1 A × X -> X) : foldr X x f nil = x.
Show proof.
assert (F := maponpaths (λ x, BinCoproductIn1 (BinCoproductsHSET _ _) · x)
(algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F tt).
(algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F tt).
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).
Show proof.
assert (F := maponpaths (λ x, BinCoproductIn2 (BinCoproductsHSET _ _) · x)
(algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F (a,,l)).
(algebra_mor_commutes _ _ _ (foldr_map X x f))).
apply (toforallpaths _ _ _ F (a,,l)).
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.
Show proof.
apply (tpair _ P').
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).
Lemma isalghom_pr1foldr :
is_algebra_mor _ List_alg List_alg (λ l, pr1 (foldr P'HSET P0' Pc' l)).
Show 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)).
- 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)).
Definition pr1foldr_algmor : algebra_mor _ List_alg List_alg :=
tpair _ _ isalghom_pr1foldr.
Lemma pr1foldr_algmor_identity : identity _ = pr1foldr_algmor.
Show proof.
Lemma listInd l : P l.
Show proof.
assert (H : pr1 (foldr P'HSET P0' Pc' l) = l).
apply (toforallpaths _ _ _ (maponpaths pr1 (!pr1foldr_algmor_identity)) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
apply (toforallpaths _ _ _ (maponpaths pr1 (!pr1foldr_algmor_identity)) l).
rewrite <- H.
apply (pr2 (foldr P'HSET P0' Pc' l)).
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.
Show proof.
Definition natHSET : HSET.
Show proof.
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.
Show proof.
apply listIndProp.
- intros l; apply isasetnat.
- apply idpath.
- simpl; unfold map, length; simpl; intros a l Hl.
simpl.
now rewrite !foldr_cons, <- Hl.
- intros l; apply isasetnat.
- apply idpath.
- simpl; unfold map, length; simpl; intros a l Hl.
simpl.
now rewrite !foldr_cons, <- Hl.
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.