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 hh 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 ff 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 IHin' (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 xh x = h' x)
(fun a f IHap (fun xin' (a; x)) (apD10^-1 IH) @
apD10 p' (a; f))).
apply (path_Algebra_Morphism H H' (apD10^-1 s)).
change (
transport
(fun hin' 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 hin' o map h) (apD10^-1 s))^ (a; f) @
(ap (fun xin' (a; x)) (apD10^-1 (fun y : B as (f y))) @
apD10 p' (a; f)) =
apD10 p' (a; f)).
rewrite apD10_V.
apply moveR_Vp.
apply whiskerR.
change (
ap (fun fin' (a; f)) (apD10^-1 (s oD f)) =
apD10 (ap (fun fin' o map f) (apD10^-1 s)) (a; f)).
rewrite <- (ap_precompose_inverse_apD10 f).
rewrite <- (ap_compose (fun hh o f) (fun fin' (a; f)) (apD10^-1 s)).
change (
ap (fun hin' (a; h o f)) (apD10^-1 s) =
ap (fun gg (a; f)) (ap (fun hin' o map h) (apD10^-1 s))).
rewrite (ap_compose (fun hin' o map h) (fun gg (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 :=
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 af 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)
Proof.
destruct w as [label arg].
- 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 bIHw b (fun af 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)
Proof.
destruct w1 as [label1 arg1]; destruct w2 as [label2 arg2]; simpl in ×.
- simpl.
- apply (@subtree_addr _ _ (sup label2 arg2) (transport B p.1 b)). simpl.
apply p.2.
Defined.

Lemma transport_addr_correct `{Funext} {A B} {w1 w2 : W A B} (p : w1 =W w2)
Proof.
rewrite <- (eissect (equiv_decode w1 w2) p).
generalize (equiv_decode w1 w2 p) as q; intros; clear.
rewrite eisretr.
destruct q.
- reflexivity.
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.
rewrite transport_forall_constant.
rewrite transport_arrow_toconst.
rewrite inv_V.
induction addr; destruct w; simpl in ×.
- reflexivity.
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.
- exact (fun wfdecorate 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.