Library Containers.W
Require Export Containers.Initial_Algebra.
Require Export Containers.Container.
Arguments sup {_ _} _ _.
Definition ap10_ap_precompose {A B C} (f : A → B) {g g' : B → C}
(p : g = g') a :
apD10 (ap (fun h ⇒ h o f) p) a = apD10 p (f a) :=
ap10_ap_precompose f p a.
Lemma ap_precompose_inverse_apD10 `{Funext} {A B C}
{f1 f2 : B → C} (g : A → B) (p : f1 == f2) :
ap (fun f ⇒ f o g) (apD10^-1 p) = apD10^-1 (p oD g).
Proof.
apply (equiv_ap apD10).
apply apD10^-1; intros x.
apply (transitivity (ap10_ap_precompose g (apD10^-1 p) x)).
rewrite eisretr.
rewrite eisretr.
reflexivity.
Qed.
Section W.
Context {funext : Funext}.
Variables (A : Type) (B : A → Type).
Let W := W A B.
Let in_ (af : (| A ||> B |) W) : W := sup af.1 af.2.
Definition W_alg := Build_Algebra (| A ||> B |) W in_.
Lemma W_initial : is_initial W_alg.
Proof.
intros [Alg in'].
set (W'_alg := Build_Algebra (| A ||> B |) Alg in').
set (h := W_rect A B (fun _ ⇒ Alg) (fun a f IH ⇒ in' (a; IH))).
set (H := Build_Algebra_Morphism W_alg W'_alg h idpath).
∃ H.
intros [h' p'].
set (H' := Build_Algebra_Morphism W_alg W'_alg h' p').
set (s :=
W_rect A B (fun x ⇒ h x = h' x)
(fun a f IH ⇒ ap (fun x ⇒ in' (a; x)) (apD10^-1 IH) @
apD10 p' (a; f))).
apply (path_Algebra_Morphism H H' (apD10^-1 s)).
change (
transport
(fun h ⇒ in' o map h = h o in_)
(apD10^-1 s)
idpath =
p').
rewrite transport_paths_FlFr.
rewrite concat_p1.
apply (equiv_ap apD10).
apply apD10^-1; intros x.
rewrite apD10_pp.
rewrite (ap10_ap_precompose in_ (apD10^-1 s) x).
rewrite eisretr.
destruct x as [a f].
change (
apD10 (ap (fun h ⇒ in' o map h) (apD10^-1 s))^ (a; f) @
(ap (fun x ⇒ in' (a; x)) (apD10^-1 (fun y : B a ⇒ s (f y))) @
apD10 p' (a; f)) =
apD10 p' (a; f)).
rewrite apD10_V.
apply moveR_Vp.
apply whiskerR.
change (
ap (fun f ⇒ in' (a; f)) (apD10^-1 (s oD f)) =
apD10 (ap (fun f ⇒ in' o map f) (apD10^-1 s)) (a; f)).
rewrite <- (ap_precompose_inverse_apD10 f).
rewrite <- (ap_compose (fun h ⇒ h o f) (fun f ⇒ in' (a; f)) (apD10^-1 s)).
change (
ap (fun h ⇒ in' (a; h o f)) (apD10^-1 s) =
ap (fun g ⇒ g (a; f)) (ap (fun h ⇒ in' o map h) (apD10^-1 s))).
rewrite (ap_compose (fun h ⇒ in' o map h) (fun g ⇒ g (a; f))).
reflexivity.
Qed.
End W.
Section Decorate_W.
Context {funext : Funext}.
Fixpoint code {A B} (w1 w2 : W A B) :=
match w1, w2 with sup a1 f1, sup a2 f2 ⇒
∃ p : a1 = a2, ∀ b, code (f1 b) (f2 (p # b))
end.
Infix "=W" := code (at level 50).
Definition equiv_decode_step {A B} (w1 w2 : W A B) :
(∃ p : w_label w1 = w_label w2, ∀ b, w_arg w1 b = w_arg w2 (p # b)) <~>
(w1 = w2).
Proof.
intros.
refine (transitivity _ (equiv_path_wtype _ _)).
refine (transitivity _ (equiv_path_sigma _ _ _)). simpl.
apply equiv_functor_sigma_id; intros p.
refine (transitivity _ (equiv_moveR_transport_p _ _ _ _)).
refine (transitivity _ (equiv_inverse (equiv_ap10 _ _))).
unfold pointwise_paths. apply equiv_functor_forall_id; intros b.
apply (equiv_concat_r).
rewrite transport_arrow_toconst.
rewrite inv_V.
reflexivity.
Defined.
Definition equiv_decode {A B} (w1 w2 : W A B) : (w1 =W w2) <~> (w1 = w2).
Proof.
revert w2; induction w1 as [a1 f1 IH]; intros [a2 f2]; simpl.
refine (transitivity _ (equiv_decode_step _ _)); simpl.
apply equiv_functor_sigma_id; intros p.
apply equiv_functor_forall_id; intros b.
apply IH.
Defined.
Inductive W_Address {A B} (w : W A B) : A → Type :=
| root_addr : W_Address w (w_label w)
| subtree_addr : ∀ child a, W_Address (w_arg w child) a → W_Address w a.
Arguments root_addr {_ _ _}.
Arguments subtree_addr {_ _ _} _ {_} _.
Fixpoint decorate {A1 A2 B} (w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
W {a1 : A1 & A2 a1} (B o pr1) :=
sup (w_label w; f (w_label w) root_addr)
(fun b : B (w_label w) ⇒ decorate (w_arg w b) (fun a ⇒ f a o subtree_addr b)).
Fixpoint undecorate1 {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) : W A1 B :=
sup (w_label w).1 (undecorate1 o w_arg w).
Fixpoint undecorate2 {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) (a : A1)
(addr : W_Address (undecorate1 w) a) {struct addr} : A2 a.
Proof.
destruct w as [label arg].
destruct addr as [ | b a addr'].
- exact label.2.
- exact (undecorate2 _ _ _ (arg b) a addr').
Defined.
Lemma undecorate1_decorate' `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
w =W undecorate1 (decorate w f).
Proof.
induction w as [label arg IHw f]; simpl.
∃ idpath. simpl.
apply (fun b ⇒ IHw b (fun a ⇒ f a o @subtree_addr _ _ (sup label arg) b a)).
Defined.
Lemma undecorate1_decorate `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
w = undecorate1 (decorate w f).
Proof.
apply equiv_decode.
apply undecorate1_decorate'.
Defined.
Fixpoint transport_addr {A B} {w1 w2 : W A B} (p : w1 =W w2) (a : A)
(addr : W_Address w1 a) {struct addr} :
W_Address w2 a.
Proof.
destruct w1 as [label1 arg1]; destruct w2 as [label2 arg2]; simpl in ×.
destruct addr as [ | b a addr'].
- simpl.
exact (transport (W_Address (sup label2 arg2)) p.1^ root_addr).
- apply (@subtree_addr _ _ (sup label2 arg2) (transport B p.1 b)). simpl.
refine (transport_addr _ _ (arg1 b) _ _ _ addr').
apply p.2.
Defined.
Lemma transport_addr_correct `{Funext} {A B} {w1 w2 : W A B} (p : w1 =W w2)
{a : A} (addr : W_Address w1 a) :
transport (fun w ⇒ W_Address w a) (equiv_decode _ _ p) addr =
transport_addr p a addr.
Proof.
rewrite <- (eissect (equiv_decode w1 w2) p).
generalize (equiv_decode w1 w2 p) as q; intros; clear.
rewrite eisretr.
destruct q.
induction addr; destruct w.
- reflexivity.
- simpl in IHaddr.
apply (ap (subtree_addr child)).
exact IHaddr.
Qed.
Lemma undecorate2_decorate `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
transport (fun w ⇒ ∀ a, W_Address w a → A2 a) (undecorate1_decorate w f) f =
undecorate2 (decorate w f).
Proof.
apply (moveR_transport_p (fun w' ⇒ ∀ a, W_Address w' a → A2 a)).
apply apD10^-1; intros a.
apply apD10^-1; intros addr.
rewrite transport_forall_constant.
rewrite transport_arrow_toconst.
rewrite inv_V.
rewrite transport_addr_correct.
induction addr; destruct w; simpl in ×.
- reflexivity.
- rewrite <- IHaddr.
reflexivity.
Qed.
Lemma decorate_undecorate `{Funext} {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) :
decorate (undecorate1 w) (undecorate2 w) = w.
Proof.
induction w as [label arg IHw].
simpl.
f_ap.
exact (apD10^-1 IHw).
Qed.
Lemma equiv_decorate `{Funext} {A1 A2 B} :
{w : W A1 B & ∀ a : A1, W_Address w a → A2 a} <~>
W {a1 : A1 & A2 a1} (B o pr1).
Proof.
serapply equiv_adjointify.
- exact (fun wf ⇒ decorate wf.1 wf.2).
- intros w.
∃ (undecorate1 w).
apply (undecorate2 w).
- exact decorate_undecorate.
- intros [w f].
serapply path_sigma; simpl.
+ symmetry.
apply undecorate1_decorate.
+ apply (moveR_transport_V (fun w0 : W A1 B ⇒ ∀ a : A1, W_Address w0 a → A2 a)).
symmetry.
apply undecorate2_decorate.
Qed.
End Decorate_W.
Require Export Containers.Container.
Arguments sup {_ _} _ _.
Definition ap10_ap_precompose {A B C} (f : A → B) {g g' : B → C}
(p : g = g') a :
apD10 (ap (fun h ⇒ h o f) p) a = apD10 p (f a) :=
ap10_ap_precompose f p a.
Lemma ap_precompose_inverse_apD10 `{Funext} {A B C}
{f1 f2 : B → C} (g : A → B) (p : f1 == f2) :
ap (fun f ⇒ f o g) (apD10^-1 p) = apD10^-1 (p oD g).
Proof.
apply (equiv_ap apD10).
apply apD10^-1; intros x.
apply (transitivity (ap10_ap_precompose g (apD10^-1 p) x)).
rewrite eisretr.
rewrite eisretr.
reflexivity.
Qed.
Section W.
Context {funext : Funext}.
Variables (A : Type) (B : A → Type).
Let W := W A B.
Let in_ (af : (| A ||> B |) W) : W := sup af.1 af.2.
Definition W_alg := Build_Algebra (| A ||> B |) W in_.
Lemma W_initial : is_initial W_alg.
Proof.
intros [Alg in'].
set (W'_alg := Build_Algebra (| A ||> B |) Alg in').
set (h := W_rect A B (fun _ ⇒ Alg) (fun a f IH ⇒ in' (a; IH))).
set (H := Build_Algebra_Morphism W_alg W'_alg h idpath).
∃ H.
intros [h' p'].
set (H' := Build_Algebra_Morphism W_alg W'_alg h' p').
set (s :=
W_rect A B (fun x ⇒ h x = h' x)
(fun a f IH ⇒ ap (fun x ⇒ in' (a; x)) (apD10^-1 IH) @
apD10 p' (a; f))).
apply (path_Algebra_Morphism H H' (apD10^-1 s)).
change (
transport
(fun h ⇒ in' o map h = h o in_)
(apD10^-1 s)
idpath =
p').
rewrite transport_paths_FlFr.
rewrite concat_p1.
apply (equiv_ap apD10).
apply apD10^-1; intros x.
rewrite apD10_pp.
rewrite (ap10_ap_precompose in_ (apD10^-1 s) x).
rewrite eisretr.
destruct x as [a f].
change (
apD10 (ap (fun h ⇒ in' o map h) (apD10^-1 s))^ (a; f) @
(ap (fun x ⇒ in' (a; x)) (apD10^-1 (fun y : B a ⇒ s (f y))) @
apD10 p' (a; f)) =
apD10 p' (a; f)).
rewrite apD10_V.
apply moveR_Vp.
apply whiskerR.
change (
ap (fun f ⇒ in' (a; f)) (apD10^-1 (s oD f)) =
apD10 (ap (fun f ⇒ in' o map f) (apD10^-1 s)) (a; f)).
rewrite <- (ap_precompose_inverse_apD10 f).
rewrite <- (ap_compose (fun h ⇒ h o f) (fun f ⇒ in' (a; f)) (apD10^-1 s)).
change (
ap (fun h ⇒ in' (a; h o f)) (apD10^-1 s) =
ap (fun g ⇒ g (a; f)) (ap (fun h ⇒ in' o map h) (apD10^-1 s))).
rewrite (ap_compose (fun h ⇒ in' o map h) (fun g ⇒ g (a; f))).
reflexivity.
Qed.
End W.
Section Decorate_W.
Context {funext : Funext}.
Fixpoint code {A B} (w1 w2 : W A B) :=
match w1, w2 with sup a1 f1, sup a2 f2 ⇒
∃ p : a1 = a2, ∀ b, code (f1 b) (f2 (p # b))
end.
Infix "=W" := code (at level 50).
Definition equiv_decode_step {A B} (w1 w2 : W A B) :
(∃ p : w_label w1 = w_label w2, ∀ b, w_arg w1 b = w_arg w2 (p # b)) <~>
(w1 = w2).
Proof.
intros.
refine (transitivity _ (equiv_path_wtype _ _)).
refine (transitivity _ (equiv_path_sigma _ _ _)). simpl.
apply equiv_functor_sigma_id; intros p.
refine (transitivity _ (equiv_moveR_transport_p _ _ _ _)).
refine (transitivity _ (equiv_inverse (equiv_ap10 _ _))).
unfold pointwise_paths. apply equiv_functor_forall_id; intros b.
apply (equiv_concat_r).
rewrite transport_arrow_toconst.
rewrite inv_V.
reflexivity.
Defined.
Definition equiv_decode {A B} (w1 w2 : W A B) : (w1 =W w2) <~> (w1 = w2).
Proof.
revert w2; induction w1 as [a1 f1 IH]; intros [a2 f2]; simpl.
refine (transitivity _ (equiv_decode_step _ _)); simpl.
apply equiv_functor_sigma_id; intros p.
apply equiv_functor_forall_id; intros b.
apply IH.
Defined.
Inductive W_Address {A B} (w : W A B) : A → Type :=
| root_addr : W_Address w (w_label w)
| subtree_addr : ∀ child a, W_Address (w_arg w child) a → W_Address w a.
Arguments root_addr {_ _ _}.
Arguments subtree_addr {_ _ _} _ {_} _.
Fixpoint decorate {A1 A2 B} (w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
W {a1 : A1 & A2 a1} (B o pr1) :=
sup (w_label w; f (w_label w) root_addr)
(fun b : B (w_label w) ⇒ decorate (w_arg w b) (fun a ⇒ f a o subtree_addr b)).
Fixpoint undecorate1 {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) : W A1 B :=
sup (w_label w).1 (undecorate1 o w_arg w).
Fixpoint undecorate2 {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) (a : A1)
(addr : W_Address (undecorate1 w) a) {struct addr} : A2 a.
Proof.
destruct w as [label arg].
destruct addr as [ | b a addr'].
- exact label.2.
- exact (undecorate2 _ _ _ (arg b) a addr').
Defined.
Lemma undecorate1_decorate' `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
w =W undecorate1 (decorate w f).
Proof.
induction w as [label arg IHw f]; simpl.
∃ idpath. simpl.
apply (fun b ⇒ IHw b (fun a ⇒ f a o @subtree_addr _ _ (sup label arg) b a)).
Defined.
Lemma undecorate1_decorate `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
w = undecorate1 (decorate w f).
Proof.
apply equiv_decode.
apply undecorate1_decorate'.
Defined.
Fixpoint transport_addr {A B} {w1 w2 : W A B} (p : w1 =W w2) (a : A)
(addr : W_Address w1 a) {struct addr} :
W_Address w2 a.
Proof.
destruct w1 as [label1 arg1]; destruct w2 as [label2 arg2]; simpl in ×.
destruct addr as [ | b a addr'].
- simpl.
exact (transport (W_Address (sup label2 arg2)) p.1^ root_addr).
- apply (@subtree_addr _ _ (sup label2 arg2) (transport B p.1 b)). simpl.
refine (transport_addr _ _ (arg1 b) _ _ _ addr').
apply p.2.
Defined.
Lemma transport_addr_correct `{Funext} {A B} {w1 w2 : W A B} (p : w1 =W w2)
{a : A} (addr : W_Address w1 a) :
transport (fun w ⇒ W_Address w a) (equiv_decode _ _ p) addr =
transport_addr p a addr.
Proof.
rewrite <- (eissect (equiv_decode w1 w2) p).
generalize (equiv_decode w1 w2 p) as q; intros; clear.
rewrite eisretr.
destruct q.
induction addr; destruct w.
- reflexivity.
- simpl in IHaddr.
apply (ap (subtree_addr child)).
exact IHaddr.
Qed.
Lemma undecorate2_decorate `{Funext} {A1 A2 B}
(w : W A1 B) (f : ∀ a, W_Address w a → A2 a) :
transport (fun w ⇒ ∀ a, W_Address w a → A2 a) (undecorate1_decorate w f) f =
undecorate2 (decorate w f).
Proof.
apply (moveR_transport_p (fun w' ⇒ ∀ a, W_Address w' a → A2 a)).
apply apD10^-1; intros a.
apply apD10^-1; intros addr.
rewrite transport_forall_constant.
rewrite transport_arrow_toconst.
rewrite inv_V.
rewrite transport_addr_correct.
induction addr; destruct w; simpl in ×.
- reflexivity.
- rewrite <- IHaddr.
reflexivity.
Qed.
Lemma decorate_undecorate `{Funext} {A1 A2 B} (w : W {a1 : A1 & A2 a1} (B o pr1)) :
decorate (undecorate1 w) (undecorate2 w) = w.
Proof.
induction w as [label arg IHw].
simpl.
f_ap.
exact (apD10^-1 IHw).
Qed.
Lemma equiv_decorate `{Funext} {A1 A2 B} :
{w : W A1 B & ∀ a : A1, W_Address w a → A2 a} <~>
W {a1 : A1 & A2 a1} (B o pr1).
Proof.
serapply equiv_adjointify.
- exact (fun wf ⇒ decorate wf.1 wf.2).
- intros w.
∃ (undecorate1 w).
apply (undecorate2 w).
- exact decorate_undecorate.
- intros [w f].
serapply path_sigma; simpl.
+ symmetry.
apply undecorate1_decorate.
+ apply (moveR_transport_V (fun w0 : W A1 B ⇒ ∀ a : A1, W_Address w0 a → A2 a)).
symmetry.
apply undecorate2_decorate.
Qed.
End Decorate_W.