### Profile

Statistics
| Branch: | Revision:

## corque / lemma_9.v @ 4806fe22

 1 ```Add LoadPath "~/Schreibtisch/svnba/Elgot/Coq/". ``` ```Require Import biCCC. ``` ```Require Import Lemmas_biCCC. ``` ```Require Import ElgotMonad. ``` ```Require Import Lemmas_ElgotMonad. ``` ```Require Import CofreeElgotMonad. ``` ```Require Import Lemmas_CofreeElgotMonad. ``` ```Require Import Coq_Steroids. ``` ```Require Import Setoid. ``` ```Open Scope c_scope. ``` ```Section ContextCofreeElgotMonad. ``` ```Context `(Co: CofreeElgotMonad). ``` ```Parameter a b : Obj. ``` ```(* --- *) ``` ```Theorem proving_kl1 : forall ``` ```(x : Obj), ``` ``` (ηv (x:=x) (a:=a) (b:=b)) § = id. ``` ```Proof. ``` ```intros. ``` ```symmetry; apply lifting2; rewrite -> id_l. ``` ```rewrite -> out_unitcofree. ``` ```rewrite -> cont_id, -> id_l. ``` ```rewrite <- f_cpr, -> inl_inr_is_id, id_l. ``` ```rewrite -> kl1, id_r; trivial. ``` ```Qed. ``` ```Theorem proving_kl2 : forall ``` ```(x y : Obj) ``` ```(f: x ~> coext T a b y), ``` ``` f § ∘ ηv (x:=x) = f. ``` ```Proof. ``` ```intros. ``` ```apply out_cong. ``` ```rewrite -> comp_assoc, lifting1. ``` ```rewrite <- comp_assoc, -> out_unitcofree. ``` ```rewrite -> comp_assoc, kl2. ``` ```rewrite -> cpr_inl; trivial. ``` ```Qed. ``` ```Theorem proving_kl3 : forall ``` ```(x y z : Obj) ``` ```(f : y ~> coext T a b z) ``` ```(g : x ~> coext T a b y), ``` ``` (f § ∘ g) § = f § ∘ g §. ``` ```Proof. ``` ```intros. ``` ```symmetry; apply lifting2. ``` ```rewrite -> comp_assoc, lifting1. ``` ```rewrite <- comp_assoc, -> lifting1. ``` ```rewrite -> comp_assoc with (f':=out); apply f_equal2; trivial. ``` ```rewrite <- kl3; apply f_equal1. ``` ```rewrite -> f_cpr. ``` ```rewrite <- comp_assoc with (f':=cont (g §)), -> comp_assoc with (g':=η), -> kl2. ``` ```rewrite -> comp_assoc with (g':=inr), cpr_inr. ``` ```rewrite <- comp_assoc with (f':=cont (g §)), -> cont_comp. ``` ```rewrite -> comp_assoc with (h':=out), -> lifting1. ``` ```rewrite -> comp_assoc with (f':=g); trivial. ``` ```Qed. ``` ```(* additional lemmas based on proving_kl1-3 *) ``` ```(* at the wrong place, change name? *) ``` ```Lemma mapc_unfold : forall ``` ```(x y : Obj) ``` ```(f:x ~> y), ``` ``` mapc f = (ηv (a:=a) (b:=b) ∘ f) §. ``` ```Proof. ``` ```intros. ``` ```unfold mapc. ``` ```symmetry; apply coit2. ``` ```rewrite -> comp_assoc, map_comp. ``` ```rewrite -> coprodhom_comp, id_r, id_l. ``` ```rewrite -> lifting1. ``` ```rewrite -> comp_assoc with (h':=out), out_unitcofree. ``` ```unfold map, coprodhom. ``` ```rewrite -> f_cpr, ->2 comp_assoc; trivial. ``` ```Qed. ``` ```Lemma liftingcofree_mapc : forall ``` ```(x y z : Obj) ``` ```(f: y ~> coext T a b z) ``` ```(g: x ~> y), ``` ``` f § ∘ mapc g = (f ∘ g) §. ``` ```Proof. ``` ```intros. ``` ```rewrite -> mapc_unfold. ``` ```rewrite <- proving_kl3. ``` ```rewrite -> comp_assoc, proving_kl2. ``` ```trivial. ``` ```Qed. ``` ```Lemma mapc_liftingcofree : forall ``` ```(x y z : Obj) ``` ```(f: y ~> z) ``` ```(g: x ~> coext T a b y), ``` ``` mapc f ∘ g § = (mapc f ∘ g) §. ``` ```Proof. ``` ```intros. ``` ```rewrite -> mapc_unfold. ``` ```rewrite <- proving_kl3. ``` ```trivial. ``` ```Qed. ``` ```(* --- *) ``` ```Theorem proving_unfolding : forall ``` ```(x y : Obj) ``` ```(f : x ~> (coext T a b (y ⊕ x))), ``` ``` [ηv , f †'] § ∘ f = f †'. ``` ```Proof. ``` ```intros. ``` ```symmetry; rewrite -> unfolding_triangle1 at 1. ``` ```unfold triangle. ``` ```rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=tuo), -> liftingcofree_tuo. ``` ```rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), <- comp_assoc with (h':=tuo), -> lifting_map. ``` ```rewrite -> cpr_coprodhom, cpr_inl, id_l. ``` ```rewrite <- unfolding. ``` ```rewrite <- comp_assoc with (h':=tuo), -> comp_assoc with (g':=(([η, ((π ∘ out) ∘ f) †]) *)). ``` ```rewrite <- kl3, -> f_cpr, -> kl2. ``` ```rewrite <- out_itercofree. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=π). ``` ```unfold π. ``` ```rewrite -> lifting_map. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, cpr_inl, id_l. ``` ```rewrite -> comp_assoc with (g':=inl), cpr_inl, cpr_inr. ``` ```rewrite ->2 comp_assoc, <- liftingcofree_tuo. ``` ```rewrite <- comp_assoc with (g':=tuo), -> tuo_out_is_id, id_l; trivial. ``` ```Qed. ``` ```(* --- *) ``` ```(* TODO: adjust name? *) ``` ```Lemma proving_naturality_h1 : forall (x y z : Obj) ``` ```(h: x ~> coext T a b (y ⊕ x)) ``` ```(g: y ~> coext T a b z), ``` ``` guarded h -> ``` ``` guarded ([mapc inl ∘ g, ηv ∘ inr] § ∘ h). ``` ```Proof. ``` ```intros. ``` ```unfold guarded in H; inversion H as [u' H1]. ``` ```unfold guarded. ``` ```exists ([map (id ⊕⊕ id ×× mapc inl ^^ id) ∘ out ∘ g, η ∘ inr ∘ ``` ``` cont (([mapc inl ∘ g, ηv ∘ inr]) §)] * ∘ u'). ``` ```rewrite -> comp_assoc, lifting1. ``` ```rewrite <- comp_assoc, -> H1. ``` ```rewrite -> comp_assoc with (f':=u'), lifting_map. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl, id_l. ``` ```rewrite -> comp_assoc, out_mapc. ``` ```rewrite -> comp_assoc with (f':=u'); apply f_equal2; trivial. ``` ```rewrite -> map_lifting; apply f_equal1. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 comp_assoc, map_comp, coprodhom_comp, id_l, id_r. ``` ```rewrite <-2 comp_assoc with (h':=η), -> comp_assoc with (g':=η), map_unit. ``` ```rewrite <- comp_assoc with (h':=η), -> comp_assoc with (h':=inl ⊕⊕ id). ``` ```rewrite -> coprodhom_inr, id_l; trivial. ``` ```Qed. ``` ```(* TODO: change name, move ? *) ``` ```Theorem proving_naturality_h2 : forall (x y z : Obj) ``` ```(f : x ~> (coext T a b (y ⊕ x))) ``` ```(g : y ~> (coext T a b z)), ``` ``` ▷(([mapc inl ∘ g, ηv ∘ inr]) § ∘ f) = (([mapc inl ∘ g, ηv ∘ inr]) § ∘ ▷f). ``` ```Proof. ``` ```intros. ``` ```set (w:=[mapc inl ∘ g, ηv ∘ inr]). ``` ```rewrite <- guardedtriangle; trivial. ``` ```unfold triangle at 2 3. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1. ``` ```rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. ``` ```rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map, -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (g':=w); unfold w at 2. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> comp_assoc with (h':=π); unfold π at 1. ``` ```rewrite -> map_lifting. ``` ```rewrite -> naturality. ``` ```rewrite <- codiagonal. ``` ```rewrite -> comp_assoc with (h':=map ([id, inr])), -> map_lifting. ``` ```rewrite -> f_cpr. ``` ```rewrite ->4 comp_assoc, ->2 map_comp. ``` ```rewrite -> cpr_inl, -> id_r. ``` ```rewrite -> comp_assoc with (g':=η), -> map_unit. ``` ```rewrite <- comp_assoc with (f':=inr), -> cpr_inr. ``` ```unfold π. ``` ```rewrite -> lifting_map. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> cpr_inr. ``` ```assert (aux: map ([inl ⊕⊕ id, inl ∘ inr]) ∘ η ∘ inl ∘ inr = ``` ``` η ∘ inr (a:=z ⊕ a × coext T a b (z ⊕ x) ^ b) (b:=x)). ``` ```rewrite -> map_unit. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl. ``` ```rewrite <- comp_assoc, -> coprodhom_inr, -> id_l. ``` ```trivial. ``` ```rewrite <- aux; clear aux. ``` ```rewrite <-2 comp_assoc with (h':=map ([inl ⊕⊕ id, inl ∘ inr])), <-2 f_cpr. ``` ```rewrite <- map_lifting. ``` ```rewrite <- out_unitcofree. ``` ```rewrite <- comp_assoc with (h':=out), <- f_cpr. ``` ```rewrite <- comp_assoc with (f':=out), <- lifting1. ``` ```rewrite -> comp_assoc with (g':=out), <- comp_assoc with (f':=f). ``` ```trivial. ``` ```apply proving_naturality_h1. ``` ```apply guardedtriangle_def. ``` ```Qed. ``` ```Theorem proving_naturality : forall ``` ```(x y z : Obj) ``` ```(f : x ~> (coext T a b (y ⊕ x))) ``` ```(g : y ~> (coext T a b z)), ``` ``` g § ∘ f †' = ([(ηv ∘ inl) § ∘ g , ηv ∘ inr] § ∘ f) †'. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold. ``` ```rewrite -> itercofree_triangle. ``` ```symmetry; rewrite -> itercofree_triangle; symmetry. ``` ```rewrite -> proving_naturality_h2. ``` ```apply unfolding_guarded2. ``` ```apply proving_naturality_h1. ``` ```apply guardedtriangle_def. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc, -> liftingcofree_mapc. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> proving_kl1, -> id_r. ``` ```rewrite -> comp_assoc, -> proving_kl2. ``` ```rewrite -> cpr_inr. ``` ```rewrite <- proving_unfolding at 1. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> proving_kl2. ``` ```trivial. ``` ```Qed. ``` ```(* --- *) ``` ```Theorem proving_dinaturality : forall ``` ```(x y z : Obj) ``` ```(g: x ~> (coext T a b (y ⊕ z))) ``` ```(h : z ~> (coext T a b (y ⊕ x))), ``` ``` ([ηv ∘ inl , h] § ∘ g) †' = ``` ``` [ ηv , ([ηv ∘ inl , g] § ∘ h) †' ] § ∘ g. ``` ```Proof. ``` ```intros. ``` ```set (s:=[ηv ∘ inl, h] § ∘ g). ``` ```set (t:=[ηv ∘ inl, g] § ∘ h). ``` ```set (w:=[ηv, t †'] § ∘ g). ``` ```set (p:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, h] §)) ⊕⊕ id (a:=z)))). ``` ```set (q:=(map ((id (a:=y) ⊕⊕ cont (a:=a) (b:=b) ([ηv ∘ inl, g] §)) ⊕⊕ id (a:=x)))). ``` ```assert (Hp: (π ∘ out ∘ s) † = ``` ``` ([η ∘ inl, π ∘ out ∘ h] * ∘ p ∘ π ∘ out ∘ g) †). ``` ```apply f_equal1. ``` ```unfold s. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```rewrite <- comp_assoc, -> lifting1. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```unfold π at 1. ``` ```rewrite -> map_lifting. ``` ```rewrite ->2 f_cpr. ``` ```rewrite -> comp_assoc with (h':=out), out_unitcofree. ``` ```rewrite -> f_cpr. ``` ```rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit. ``` ```rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl. ``` ```rewrite -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (g':=inr),-> comp_assoc with (g':=η), map_unit. ``` ```rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), cpr_inr. ``` ```unfold p, π. ``` ```rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp, id_l. ``` ```rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l. ``` ```rewrite -> comp_assoc with (g':=inl). ``` ```rewrite -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```rewrite -> lifting_map; apply f_equal1. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, id_l. ``` ```rewrite -> comp_assoc with (g':=inl), cpr_inl. ``` ```rewrite ->4 comp_assoc; trivial. ``` ```assert (Hq: (π ∘ out ∘ t) † = ``` ``` ([η ∘ inl, π ∘ out ∘ g] * ∘ q ∘ π ∘ out ∘ h) †). ``` ```apply f_equal1. ``` ```unfold t. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```rewrite <- comp_assoc, -> lifting1. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```unfold π at 1. ``` ```rewrite -> map_lifting. ``` ```rewrite ->2 f_cpr. ``` ```rewrite -> comp_assoc with (h':=out), -> out_unitcofree. ``` ```rewrite -> f_cpr. ``` ```rewrite <- comp_assoc with (f':=inl), -> comp_assoc with (g':=η), map_unit. ``` ```rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inl), cpr_inl. ``` ```rewrite -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit. ``` ```rewrite <- comp_assoc with (h':=η), -> comp_assoc with (g':=inr), -> cpr_inr. ``` ```unfold q, π. ``` ```rewrite <- comp_assoc with (f':=map ([inl ⊕⊕ id, inl ∘ inr])), -> map_comp. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), coprodhom_inl, id_l. ``` ```rewrite -> comp_assoc with (g':=inl), coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), coprodhom_inr. ``` ```rewrite -> lifting_map; apply f_equal1. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, id_l. ``` ```rewrite -> comp_assoc with (g':=inl), cpr_inl. ``` ```rewrite ->4 comp_assoc; trivial. ``` ```assert (H_main: [ηv, w] § ∘ ▷ s = [ηv, t †'] § ∘ [ ηv ∘ inl , ▷ t] § ∘ g). ``` ```(* left-hand side *) ``` ```apply out_cong. ``` ```rewrite -> comp_assoc, -> lifting1 at 1. ``` ```unfold triangle at 1. ``` ```rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), comp_assoc with (g':=tuo); ``` ```rewrite -> out_tuo_is_id, id_r. ``` ```rewrite -> comp_assoc, lifting_map. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl. ``` ```rewrite -> out_unitcofree, id_l. ``` ```rewrite -> Hp. ``` ```rewrite <- comp_assoc with (g':=p), <- comp_assoc with (f':=g), <- comp_assoc with (f':=out ∘ g). ``` ```rewrite -> dinaturality. ``` ```unfold p at 2. ``` ```rewrite <- comp_assoc with (h':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id))); ``` ```rewrite -> comp_assoc with (g':=map ((id ⊕⊕ cont (([ηv ∘ inl, h]) §) ⊕⊕ id))); ``` ```rewrite -> lifting_map. ``` ```rewrite -> cpr_coprodhom, id_l. ``` ```rewrite -> comp_assoc, <- kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=η), kl2. ``` ```rewrite -> cpr_coprodhom, id_l. ``` ```rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp. ``` ```rewrite <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=ηv), proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```assert (aux1: t †' = ([ηv, w]) § ∘ h). ``` ```rewrite <- proving_unfolding. ``` ```unfold w, t. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (f':=inl), -> proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```trivial. ``` ```rewrite <- aux1. ``` ```(* right-hand side *) ``` ```rewrite -> comp_assoc with (h':=out), -> lifting1. ``` ```rewrite <-2 comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> lifting1. ``` ```assert (aux2: (([out ∘ [ηv ∘ inl, ▷t], η ∘ inr ∘ cont (([ηv ∘ inl, ▷t]) §)]) * ``` ``` = ([η ∘ (inl ⊕⊕ cont (([ηv ∘ inl, ▷t]) §)), out ∘ ▷t] * ∘ π))). ``` ```unfold π. ``` ```rewrite -> lifting_map. ``` ```rewrite ->2 f_cpr. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl, id_l. ``` ```rewrite ->2 comp_assoc with (g':=inl), cpr_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```rewrite -> comp_assoc with (h':=out), out_unitcofree. ``` ```rewrite -> comp_assoc;trivial. ``` ```rewrite <- comp_assoc with (f':=g), -> aux2; clear aux2. ``` ```rewrite <-2 comp_assoc with (g':=π), -> comp_assoc with (f':=π ∘ (out ∘ g)), <- kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=η), kl2. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (h':=η ∘ inr), -> cont_comp. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl. ``` ```rewrite -> out_unitcofree. ``` ```rewrite <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (f':=inl), proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```rewrite <- unfolding_triangle1. ``` ```apply f_equal2;trivial. ``` ```apply f_equal1. ``` ```apply f_equal2;trivial. ``` ```(* left-hand side *) ``` ```rewrite -> naturality. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=η), map_unit. ``` ```rewrite <- comp_assoc with (g':=inr), -> comp_assoc with (g':=η), -> map_unit. ``` ```rewrite -> comp_assoc, <- kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=η), kl2. ``` ```rewrite -> cpr_inl. ``` ```rewrite <- f_cpr. ``` ```rewrite -> comp_assoc with (g':=p); unfold p. ``` ```rewrite -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (f':=id ⊕⊕ cont (([ηv ∘ inl, h]) §)), -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (f':=cont (([ηv ∘ inl, h]) §)), -> cont_comp. ``` ```rewrite <- proving_kl3. ``` ```rewrite -> f_cpr with (f:=([ηv, w]) §). ``` ```rewrite -> comp_assoc with (g':=ηv), -> proving_kl2, -> cpr_inl. ``` ```rewrite <- aux1. ``` ```assert (aux3: ([(η ∘ inl) ∘ ([inl, inr ∘ cont (([ηv, t †']) §)]), η ∘ inr]) * ``` ``` ∘ η ∘ inl ∘ (id ⊕⊕ cont ([ηv ∘ inl, g] §)) ``` ``` = (η ∘ inl (b:=z)) ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, w]) §)])). ``` ```rewrite -> kl2. ``` ```rewrite -> cpr_inl. ``` ```rewrite <- comp_assoc, -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (h':=inr), -> cont_comp. ``` ```rewrite <- proving_kl3. ``` ```rewrite -> f_cpr with (f:=([ηv, t †']) §). ``` ```rewrite -> comp_assoc with (f':=inl), -> proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```trivial. ``` ```rewrite <- aux3; clear aux3. ``` ```rewrite <-2 comp_assoc, <- f_cpr. ``` ```rewrite <- comp_assoc with (h':=η), <- f_cpr. ``` ```assert (aux4: map (([inl, inr ∘ cont (([ηv, t †']) §)]) ⊕⊕ id) = ``` ``` (η ∘ ([inl ∘ ([inl, inr (a:=y) ∘ cont (a:=a) (b:=b) (([ηv, t †']) §)]), inr (b:=z)])) *). ``` ```unfold map, coprodhom; rewrite -> id_l. ``` ```trivial. ``` ```rewrite <- aux4; clear aux4. ``` ```rewrite <- map_lifting, <- comp_assoc, <- map_naturality. ``` ```(* right-hand side *) ``` ```unfold triangle. ``` ```rewrite <- comp_assoc with (h':=tuo), <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo); ``` ```rewrite -> out_tuo_is_id, id_r. ``` ```rewrite -> comp_assoc with (g':=map (inl ⊕⊕ id)), -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl. ``` ```rewrite -> out_unitcofree. ``` ```apply f_equal2. ``` ```unfold map; rewrite -> f_cpr. ``` ```rewrite -> comp_assoc; trivial. ``` ```rewrite -> comp_assoc with (f':=t), -> Hq. ``` ```unfold q. ``` ```rewrite -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite ->4 comp_assoc; trivial. ``` ```symmetry. ``` ```apply unfolding_triangle2. ``` ```rewrite -> H_main. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (f':=inl), proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```rewrite <- unfolding_triangle1. ``` ```trivial. ``` ```Qed. ``` ```(* --- *) ``` ```(* proving codiagonal, split in multiple lemmas/theorems *) ``` ```Definition ξ (x y : Obj) := ``` ```([inl ⊕⊕ id, inl (b:=x) ∘ inr (a:=y) (b:=x)]). ``` ```Arguments ξ [x y]. ``` ```Lemma ξ1 : forall (x y : Obj), ``` ```mapc ξ ∘ mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y)) = id. ``` ```Proof. ``` ```intros. ``` ```rewrite -> mapc_comp. ``` ```unfold ξ. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite -> coprodhom_inr, -> id_l. ``` ```rewrite <- f_cpr. ``` ```rewrite -> inl_inr_is_id, -> id_l. ``` ```rewrite -> inl_inr_is_id. ``` ```apply mapc_id. ``` ```Qed. ``` ```Lemma ξ2 : forall (x y : Obj), ``` ```mapc ([id, inr]) ∘ mapc (ξ (x:=x) (y:=y)) = mapc (a:=a) (b:=b) ([id, inr]). ``` ```Proof. ``` ```intros. ``` ```rewrite -> mapc_comp. ``` ```unfold ξ. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, -> id_l, id_r. ``` ```rewrite -> inl_inr_is_id. ``` ```rewrite -> comp_assoc, -> cpr_inl, -> id_r. ``` ```trivial. ``` ```Qed. ``` ```(* A.11 *) ``` ```Lemma proving_codiagonal_h0 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x))) ``` ```(h': x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ``` (h' †') †' = ([ηv, (h' †') †']) § ∘ ▷(mapc ([id, inr]) ∘ g') -> ``` ``` (h' †') †' = (mapc ([id, inr]) ∘ g') †'. ``` ```Proof. ``` ```intros. ``` ```rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ g'). ``` ```apply unfolding_guarded2. ``` ```apply guardedtriangle_def. ``` ```exact H. ``` ```Qed. ``` ```Theorem proving_codiagonal_clause1 : forall (x y : Obj) (g': x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ```guarded (mapc ([id, inr]) ∘ g') -> ``` ``` (g' †') †' = ([ηv, (g' †') †']) § ∘ ▷(mapc ([id, inr]) ∘ g'). ``` ```Proof. ``` ```intros. ``` ```rewrite <- proving_unfolding at 1. ``` ```assert (aux:([ηv, (g' †') †']) § ∘ g' †' = [ηv, (g' †') †'] § ∘ [ηv, g' †'] § ∘ g'). ``` ```symmetry; rewrite -> proving_unfolding at 1; trivial. ``` ```rewrite -> aux at 1; clear aux. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> proving_kl2. ``` ```rewrite -> proving_unfolding. ``` ```rewrite -> guardedtriangle with (f':=mapc ([id, inr]) ∘ g'); trivial. ``` ```rewrite -> comp_assoc, -> liftingcofree_mapc. ``` ```rewrite -> f_cpr, -> id_l. ``` ```rewrite -> cpr_inr. ``` ```trivial. ``` ```Qed. ``` ```(* A.10 *) ``` ```Lemma proving_codiagonal_h1 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ``` ▷(mapc ([id, inr]) ∘ ▷g) = ▷(mapc ([id, inr]) ∘ g). ``` ```Proof. ``` ```intros. ``` ```apply out_cong. ``` ```rewrite ->2 out_triangle. ``` ```rewrite <-2 comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc. ``` ```rewrite ->4 comp_assoc, -> map_comp. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> f_cpr, -> id_l. ``` ```rewrite -> cpr_inr. ``` ```rewrite <- comp_assoc, -> out_triangle. ``` ```rewrite -> map_naturality. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```rewrite <- codiagonal. ``` ```apply f_equal1. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```apply f_equal2;trivial; apply f_equal2;trivial. ``` ```unfold map. ``` ```apply f_equal1. ``` ```rewrite <- comp_assoc; apply f_equal2;trivial. ``` ```case_distinction. ``` ```case_distinction. ``` ```rewrite ->3 comp_assoc, <- comp_assoc with (h':=([id, inr])), -> coprodhom_inl. ``` ```rewrite -> comp_assoc, -> cpr_inl. ``` ```rewrite -> id_r, -> cpr_inl. ``` ```rewrite -> cpr_inl. ``` ```trivial. ``` ```rewrite -> coprodhom_inr, -> id_l. ``` ```rewrite -> cpr_inr. ``` ```trivial. ``` ```rewrite -> comp_assoc with (f':=inr), -> coprodhom_inl. ``` ```rewrite ->2 comp_assoc, -> cpr_inl, -> id_r. ``` ```rewrite -> cpr_inr. ``` ```trivial. ``` ```Qed. ``` ```Theorem proving_codiagonal_clause2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ``` guarded (mapc ξ ∘ g) -> ``` ``` (g †') †' = ▷(mapc ([id, inr]) ∘ g) †'. ``` ```Proof. ``` ```intros. ``` ```rewrite <- itercofree_triangle. ``` ```apply proving_codiagonal_h0. ``` ```rewrite <- proving_codiagonal_h1. ``` ```assert (aux: (g †') †' = (▷g †') †'). ``` ```rewrite <- itercofree_triangle;trivial. ``` ```rewrite -> aux; clear aux. ``` ```apply proving_codiagonal_clause1. ``` ```unfold guarded in H. ``` ```inversion H as [u' H']. ``` ```assert (aux1: g = mapc ξ ∘ tuo ∘ map (inl ⊕⊕ id) ∘ u'). ``` ```rewrite <- comp_assoc, <- H'. ``` ```rewrite <- comp_assoc with (g':=tuo), -> comp_assoc with (g':=out), -> tuo_out_is_id, -> id_r. ``` ```rewrite -> comp_assoc, -> ξ1, -> id_r. ``` ```trivial. ``` ```unfold guarded. ``` ```rewrite -> aux1; clear aux1. ``` ```unfold triangle. ``` ```rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=mapc ξ), ``` ``` -> comp_assoc with (g':=mapc ξ), -> out_mapc. ``` ```rewrite <- comp_assoc with (g':=out), <-2 comp_assoc with (h':=tuo), ``` ``` -> comp_assoc with (f':=map (inl ⊕⊕ id) ∘ u'), -> out_tuo_is_id, -> id_r. ``` ```rewrite -> comp_assoc with (h':=map (ξ ⊕⊕ cont (mapc ξ))), -> map_comp. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```(* ``` ```assert (aux2: map ((inl ⊕⊕ id) ⊕⊕ id) ∘ π = π ∘ map (ξ (x:=x) (y:=y) ∘ inl ``` ``` ⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (ξ (x:=x) (y:=y))))). ``` ```unfold π. ``` ```rewrite ->2 map_comp. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite -> coprodhom_inl. ``` ```(* is this even true ? see paper *) ``` ```*) ``` ```rewrite -> comp_assoc, -> out_mapc. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite -> coprodhom_comp, -> cpr_inl, -> id_l. ``` ```rewrite -> map_naturality. ``` ```rewrite -> comp_assoc; unfold π. ``` ```rewrite -> comp_assoc, ->2 map_comp. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp. ``` ```rewrite -> coprodhom_inl, ->2 id_l. ``` ```rewrite -> comp_assoc, -> coprodhom_inl. ``` ```rewrite <- comp_assoc, -> coprodhom_inr. ``` ```rewrite -> cpr_coprodhom. ``` ```unfold ξ at 1; rewrite -> cpr_inl. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite <-2 comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. ``` ```rewrite -> ξ2. ``` ```exists (map (id ⊕⊕ cont (mapc ([id, inr]))) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ u') †). ``` ```rewrite ->2 map_naturality. ``` ```apply f_equal1. ``` ```rewrite ->3 comp_assoc, ->2 map_comp. ``` ```apply f_equal2; trivial. ``` ```apply f_equal1. ``` ```rewrite ->2 coprodhom_comp, ->2 id_l, -> id_r. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```rewrite -> comp_assoc, -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```rewrite -> comp_assoc; trivial. ``` ```Qed. ``` ```(* A.12 *) ``` ```Theorem proving_codiagonal_h2 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ``` guarded g -> ``` ``` ▷(g †') = [ηv, g †'] § ∘ mapc ξ ∘ ▷ (mapc ξ ∘ g). ``` ```Proof. ``` ```intros. ``` ```apply out_cong. ``` ```(* right-hand side *) ``` ```rewrite ->2 comp_assoc, -> lifting1. ``` ```unfold triangle at 2. ``` ```rewrite <- comp_assoc with (g':=out), -> out_mapc. ``` ```rewrite -> comp_assoc with (f':=out), <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), ``` ```-> out_tuo_is_id, -> id_r. ``` ```rewrite -> lifting_map. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```unfold ξ at 1. ``` ```rewrite <- comp_assoc with (f':=inl), -> cpr_inl. ``` ```rewrite <- comp_assoc with (h':=out), -> cpr_coprodhom, -> id_l. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. ``` ```rewrite -> naturality. ``` ```rewrite ->3 f_cpr. ``` ```rewrite -> comp_assoc with (h':=out), -> out_unitcofree. ``` ```rewrite ->5 comp_assoc with (h':=map inl), -> map_unit. ``` ```unfold π. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite -> cpr_inr. ``` ```unfold guarded in H. ``` ```inversion H as [u' H']. ``` ```rewrite <- comp_assoc with (f':=g), -> H'. ``` ```rewrite -> comp_assoc with (f':=u'), -> map_comp, -> coprodhom_comp, -> id_l. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite <- comp_assoc with (f':=cont (mapc ξ)), -> cont_comp. ``` ```unfold ξ at 1. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> cpr_inl. ``` ```rewrite <- comp_assoc with (g':=mapc ξ), -> ξ1, -> id_l. ``` ```(* left-hand side *) ``` ```unfold triangle. ``` ```rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r. ``` ```rewrite -> map_naturality. ``` ```unfold π. ``` ```rewrite ->2 comp_assoc, -> map_comp, -> f_cpr. ``` ```rewrite -> coprodhom_comp, -> coprodhom_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr, -> id_l. ``` ```rewrite <- comp_assoc with (g':=out), <- proving_unfolding at 1. ``` ```rewrite -> comp_assoc with (h':=out), -> lifting1. ``` ```rewrite -> f_cpr, -> out_unitcofree. ``` ```rewrite <- comp_assoc with (f':=g), -> H'. ``` ```rewrite -> comp_assoc with (f':=u'), -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> comp_assoc with (f':=u'), -> map_lifting, -> f_cpr. ``` ```rewrite ->3 comp_assoc, -> map_unit. ``` ```rewrite <-2 comp_assoc with (h':=η), -> cpr_inl, -> cpr_inr. ``` ```unfold coprodhom. ``` ```rewrite -> f_cpr, -> id_l, ->3 comp_assoc. ``` ```trivial. ``` ```Qed. ``` ```Theorem proving_codiagonal_h3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ```guarded g -> ``` ```(g †') †' = (([ηv ∘ inl, g †']) § ∘ (mapc ξ ∘ g) †') †'. ``` ```Proof. ``` ```intros. ``` ```set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). ``` ```rewrite -> itercofree_triangle at 1. ``` ```rewrite -> proving_codiagonal_h2. ``` ```rewrite <- id_l with (f':=ηv). ``` ```rewrite <- inl_inr_is_id. ``` ```rewrite -> f_cpr. ``` ```rewrite -> liftingcofree_mapc. ``` ```unfold ξ at 1. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> cpr_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite -> cpr_inr. ``` ```assert (aux1: mapc ([id, inr]) ∘ ([[ηv ∘ inl ∘ inl, mapc inl ∘ g †'], ηv ∘ inr]) § ``` ``` = ([[ηv ∘ inl, g †'], ηv ∘ inr]) §). ``` ```rewrite -> mapc_liftingcofree. ``` ```rewrite ->2 f_cpr. ``` ```rewrite ->2 comp_assoc, -> mapc_unitcofree. ``` ```rewrite <- comp_assoc with (g':=[id, inr]), -> cpr_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=mapc inl), -> mapc_comp. ``` ```rewrite -> cpr_inl, -> mapc_id, -> id_r. ``` ```rewrite -> comp_assoc, -> mapc_unitcofree. ``` ```rewrite <- comp_assoc, -> cpr_inr. ``` ```trivial. ``` ```rewrite <- aux1; clear aux1. ``` ```rewrite -> itercofree_triangle. ``` ```rewrite <- comp_assoc, <- proving_codiagonal_clause2. ``` ```assert (aux2: mapc inl ∘ ([ηv ∘ inl, g †']) = [(ηv ∘ inl) ∘ inl, mapc (inl (b:=x)) ∘ g †']). ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc, -> mapc_unitcofree. ``` ```trivial. ``` ```rewrite <- aux2; clear aux2. ``` ```rewrite -> mapc_unfold at 1. ``` ```rewrite <- proving_naturality. ``` ```rewrite <- itercofree_triangle. ``` ```trivial. ``` ```unfold guarded. ``` ```assert (aux4: exists u : x ~> T (y ⊕ a × coext T a b ((y ⊕ x) ⊕ x) ^ b), out∘ ▷(mapc ξ ∘ g) = map (inl ∘ inl ⊕⊕ id) ∘ u). ``` ```unfold triangle. ``` ```rewrite ->2 comp_assoc, -> out_tuo_is_id, -> id_r. ``` ```rewrite -> comp_assoc, <- comp_assoc with (g':=out), -> out_mapc. ``` ```rewrite -> comp_assoc; unfold π. ``` ```rewrite -> map_comp. ``` ```rewrite -> cpr_coprodhom. ``` ```unfold ξ. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp, -> id_r. ``` ```rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl, <- comp_assoc with (g':=out). ``` ```unfold guarded in H. ``` ```inversion H as [z Q]. ``` ```rewrite -> Q. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> cpr_inl. ``` ```unfold coprodhom at 2; rewrite -> id_l. ``` ```assert (aux5: z = π ∘ π ∘ z). ``` ```unfold π. ``` ```rewrite -> map_comp. ``` ```unfold coprodhom. ``` ```coprod_simp. ``` ```rewrite ->2 id_l. ``` ```rewrite <- f_cpr. ``` ```rewrite -> inl_inr_is_id, -> id_l. ``` ```rewrite -> inl_inr_is_id, -> map_id, -> id_r; trivial. ``` ```rewrite -> aux5; clear aux5. ``` ```rewrite <- comp_assoc with (g':=π), -> comp_assoc with (g':=π); ``` ```unfold π at 1. ``` ```rewrite -> map_comp. ``` ```rewrite -> f_cpr. ``` ```rewrite -> cpr_coprodhom, -> cpr_inl, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl) (f':=inr), -> cpr_inl. ``` ```rewrite -> cpr_inr, <- comp_assoc with (h':=inl) (g':=inr). ``` ```rewrite <- f_cpr. ``` ```unfold map at 2. ``` ```rewrite -> f_cpr with (f:=η). ``` ```rewrite <- map_unit. ``` ```rewrite <- map_comp, <- comp_assoc with (h':=map inl). ``` ```rewrite <- naturality. ``` ```rewrite -> comp_assoc, -> map_lifting. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```unfold coprodhom at 1. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite -> comp_assoc with (g':=inr), -> cpr_inr, -> id_l. ``` ```rewrite <- comp_assoc with (g':=inl), <- map_lifting. ``` ```rewrite -> kl1, -> id_l. ``` ```exists (map (id ⊕⊕ cont (mapc ([inl ⊕⊕ id, inl ∘ inr]))) ∘ (π ∘ z) †). ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```unfold coprodhom. ``` ```coprod_simp. ``` ```rewrite ->3 id_l, -> comp_assoc. ``` ```trivial. ``` ```inversion aux4 as [w H']. ``` ```rewrite -> comp_assoc with (h':=mapc ξ). ``` ```rewrite -> mapc_liftingcofree. ``` ```rewrite ->2 f_cpr. ``` ```rewrite ->4 comp_assoc with (h':=mapc ξ), -> mapc_unitcofree, -> mapc_comp. ``` ```rewrite <-2 comp_assoc with (g':=ξ). ``` ```unfold ξ at 1 2 3. ``` ```rewrite -> cpr_inl, -> cpr_inr. ``` ```rewrite <- comp_assoc with (f':=inl), -> coprodhom_inl. ``` ```rewrite -> comp_assoc, -> lifting1. ``` ```rewrite ->2 f_cpr. ``` ```rewrite <- comp_assoc with (g':=out), -> H'. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> comp_assoc with (g':=inl), ->2 cpr_inl. ``` ```rewrite -> comp_assoc with (h':=out), -> out_unitcofree. ``` ```rewrite -> comp_assoc. ``` ```rewrite <- cpr_coprodhom with (f:=(η ∘ inl) ∘ inl) (i:=cont ``` ``` (([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'], ηv ∘ (inl ∘ inr)]) §)). ``` ```rewrite <- comp_assoc, <- f_cpr. ``` ```rewrite <- map_unit. ``` ```rewrite <- comp_assoc with (g':=η). ``` ```rewrite <- map_lifting. ``` ```rewrite <- comp_assoc with (h':=map ([inl ∘ inl, inr])). ``` ```exists ((η ∘ (inl ⊕⊕ cont (([[ηv ∘ (inl ∘ inl), mapc (inl ⊕⊕ id) ∘ g †'], ``` ``` ηv ∘ (inl ∘ inr)]) §))) * ∘ w). ``` ```unfold coprodhom at 3. ``` ```rewrite -> id_l. ``` ```trivial. ``` ```exact H. ``` ```Qed. ``` ```Theorem proving_codiagonal_h4 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ```guarded g -> ``` ```((mapc ξ ∘ g) †') †' = (g †') †'. ``` ```Proof. ``` ```intros. ``` ```set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). ``` ```symmetry. ``` ```apply unfolding_guarded2. ``` ```unfold guarded. ``` ```unfold guarded in H. ``` ```inversion H as [u' H']. ``` ```exists (map (id ⊕⊕ cont ([ηv,( mapc ξ ∘ g) †'] §) ) ∘ (map ([inl ⊕⊕ id, inl ∘ inr]) ∘ map (id ⊕⊕ cont (mapc ξ)) ∘ u') †). ``` ```rewrite -> out_itercofree. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. ``` ```rewrite <- comp_assoc with (g':=out), -> H'. ``` ```rewrite -> naturality. ``` ```rewrite -> map_naturality. ``` ```rewrite -> map_naturality. ``` ```apply f_equal1. ``` ```unfold π. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> comp_assoc, -> lifting_map. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite ->2 comp_assoc, ->2 map_comp. ``` ```apply f_equal2; trivial. ``` ```rewrite -> f_cpr. ``` ```rewrite ->3 cpr_coprodhom. ``` ```rewrite -> id_l. ``` ```rewrite ->2 coprodhom_comp. ``` ```rewrite ->2 id_l, ->2 id_r. ``` ```rewrite -> f_cpr with (f:=(inl ⊕⊕ cont (([ηv, (mapc ξ ∘ g) †']) §)) ⊕⊕ id). ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> id_l. ``` ```unfold map. ``` ```apply f_equal1. ``` ```case_distinction. ``` ```rewrite <- comp_assoc with (f':=inl). ``` ```rewrite -> cpr_inl. ``` ```rewrite -> coprodhom_comp. ``` ```rewrite -> coprodhom_inl. ``` ```unfold ξ. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> comp_assoc, -> kl2. ``` ```unfold coprodhom. ``` ```rewrite -> f_cpr. ``` ```rewrite ->3 id_l. ``` ```rewrite ->2 comp_assoc. ``` ```trivial. ``` ```rewrite <- comp_assoc with (f':=inr). ``` ```rewrite ->2 cpr_inr. ``` ```rewrite -> comp_assoc with (g':=inl), -> cpr_inl. ``` ```rewrite <- comp_assoc with (f':=inr). ``` ```rewrite -> cpr_inr. ``` ```rewrite ->2 comp_assoc, -> kl2. ``` ```rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. ``` ```rewrite <-2 comp_assoc with (f':=inr). ``` ```rewrite -> coprodhom_inr. ``` ```rewrite ->4 comp_assoc. ``` ```trivial. (* this might be possible in a much simpler way *) ``` ```rewrite -> proving_codiagonal_h3 at 1. ``` ```rewrite <- proving_unfolding at 1. ``` ```rewrite <- proving_codiagonal_h3. ``` ```rewrite -> comp_assoc, <- proving_kl3. ``` ```rewrite -> f_cpr. ``` ```rewrite -> comp_assoc, -> proving_kl2. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> proving_unfolding. ``` ```trivial. ``` ```exact H. ``` ```exact H. ``` ```Qed. ``` ```Theorem proving_codiagonal_clause3 : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ```guarded g -> ``` ```(mapc ([id, inr]) ∘ g) †' = (g †') †'. ``` ```Proof. ``` ```intros. ``` ```set (h:= mapc ξ ∘ ▷ (mapc ξ ∘ g)). ``` ```transitivity (((mapc ξ ∘ g) †') †'). ``` ```rewrite -> proving_codiagonal_clause2. ``` ```rewrite <- itercofree_triangle. ``` ```rewrite -> comp_assoc, -> ξ2. ``` ```trivial. ``` ```unfold guarded. ``` ```rewrite -> comp_assoc with (f':=g), -> ξ1, -> id_r. ``` ```exact H. ``` ```apply proving_codiagonal_h4. ``` ```apply H. ``` ```Qed. ``` ```Theorem proving_codiagonal : forall (x y : Obj) (g: x ~> (coext T a b (y ⊕ x ⊕ x))), ``` ``` ((ηv ∘ ([id, inr])) § ∘ g) †' = (g †') †'. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold. ``` ```(* clause 4 *) ``` ```set (h:= mapc ξ ∘ ▷ g). ``` ```transitivity (((mapc ξ ∘ h) †') †'). ``` ```rewrite <- proving_codiagonal_clause3. ``` ```rewrite -> comp_assoc, ξ2. ``` ```unfold h. ``` ```rewrite -> comp_assoc, ξ2. ``` ```rewrite -> itercofree_triangle with (f:=mapc ([id, inr]) ∘ ▷g). ``` ```rewrite -> proving_codiagonal_h1. ``` ```apply itercofree_triangle. ``` ```unfold h. ``` ```rewrite -> comp_assoc, -> ξ1, -> id_r. ``` ```apply guardedtriangle_def. ``` ```unfold h. ``` ```rewrite -> comp_assoc, -> ξ1, -> id_r. ``` ```rewrite <- itercofree_triangle. ``` ```trivial. ``` ```Qed. ``` ```(* --- *) ``` ```Theorem proving_uniformity_guarded : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x), ``` ``` guarded g -> ``` ``` f ∘ h = mapc (id ⊕⊕ h) ∘ g -> ``` ``` f †' ∘ h = g †'. ``` ```Proof. ``` ```intros. ``` ```apply unfolding_guarded2. ``` ```apply H. ``` ```assert (aux: ([ηv, f †' ∘ h]) § = ([ηv, f †']) § ∘ mapc (id ⊕⊕ h)). ``` ```rewrite -> liftingcofree_mapc. ``` ```rewrite -> cpr_coprodhom, id_l; trivial. ``` ```rewrite -> aux. ``` ```rewrite <- comp_assoc, <- H0. ``` ```rewrite -> comp_assoc, -> proving_unfolding. ``` ```trivial. ``` ```Qed. ``` ```Theorem proving_uniformity : forall x y z (f : x ~> coext T a b (y ⊕ x)) (g: z ~> coext T a b (y ⊕ z)) (h: z ~> x), ``` ``` f ∘ h = (ηv ∘ (id ⊕⊕ h)) § ∘ g -> ``` ``` f †' ∘ h = g †'. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold in H. ``` ```assert (H1: (π ∘ out ∘ f) † ∘ h = ``` ``` map (id ⊕⊕ cont (mapc (id ⊕⊕ h))) ∘ (π ∘ out ∘ g) †). ``` ```rewrite -> map_naturality. ``` ```apply uniformity. ``` ```rewrite <- comp_assoc, -> H. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> out_mapc. ``` ```rewrite <-2 comp_assoc with (f':=g), ->3 comp_assoc with (f':=out ∘ g); ``` ```apply f_equal2;trivial. ``` ```unfold π. ``` ```rewrite ->3 map_comp. ``` ```apply f_equal1. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> coprodhom_comp, -> id_l, -> id_r. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```rewrite -> comp_assoc, -> coprodhom_inl. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```rewrite -> f_cpr. ``` ```rewrite -> coprodhom_comp, -> id_l, -> id_r. ``` ```rewrite -> comp_assoc, -> coprodhom_inl, -> id_l. ``` ```rewrite -> comp_assoc; trivial. ``` ```assert (H2: (▷f) ∘ h = mapc (id ⊕⊕ h) ∘ ▷g). ``` ```unfold triangle. ``` ```rewrite <- comp_assoc, -> H1. ``` ```rewrite ->2 comp_assoc; apply f_equal2; trivial. ``` ```apply out_cong. ``` ```rewrite -> comp_assoc with (g':=mapc (id ⊕⊕ h)), -> out_mapc. ``` ```rewrite ->2 comp_assoc with (h':=out), -> out_tuo_is_id, -> id_r. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (g':=tuo), -> out_tuo_is_id, -> id_r. ``` ```rewrite ->2 map_comp. ``` ```rewrite ->2 coprodhom_comp, -> id_l. ``` ```rewrite -> coprodhom_inl. ``` ```rewrite ->2 id_l, -> id_r; trivial. ``` ```rewrite -> itercofree_triangle. ``` ```symmetry; rewrite -> itercofree_triangle; symmetry. ``` ```apply proving_uniformity_guarded. ``` ```apply guardedtriangle_def. ``` ```apply H2. ``` ```Qed. ``` ```(* --- *) ``` ```Theorem proving_str1 : forall ``` ```(x : Obj), ``` ``` pr2 (a:=terminal_obj) (b:=coext T a b x) = (ηv ∘ pr2) § ∘ τv. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold. ``` ```assert (H1: pr2 (a:=terminal_obj) (b:=coext T a b x) = mapc pr2 ∘ (mapc (pair bang id) ∘ pr2)). ``` ```rewrite -> comp_assoc, -> mapc_comp. ``` ```rewrite -> pr2_pair. ``` ```rewrite -> mapc_id, -> id_r. ``` ```trivial. ``` ```rewrite -> H1. ``` ```apply f_equal2;trivial. ``` ```apply strength2. ``` ```assert (H2: id (a:=terminal_obj × x) = (pair bang id) ∘ pr2). ``` ```rewrite -> pair_f, -> id_r. ``` ```assert (aux1: bang ∘ pr2 (a:=terminal_obj) (b:=x) = pr1). ``` ```transitivity (bang (a:=terminal_obj × x)). ``` ```apply bang_axiom. ``` ```symmetry; apply bang_axiom. ``` ```rewrite -> aux1; clear aux1. ``` ```symmetry; apply pr1_pr2_is_id. ``` ```rewrite -> H2. ``` ```rewrite -> map_comp. ``` ```assert (aux2: ((pair bang id) ∘ pr2 (a:=terminal_obj) (b:=x) ⊕⊕ cont (mapc (pair bang id) ∘ pr2)) ∘ δ = ``` ``` ((pair bang id) ⊕⊕ cont (a:=a) (b:=b) (mapc (a:=a) (b:=b) (pair bang id (a:=x)))) ∘ pr2). ``` ```set (y:=(pair bang id)). ``` ```rewrite <-2 pr2_prodhom with (f:=id). ``` ```rewrite <- cont_comp. ``` ```rewrite <- coprodhom_comp. ``` ```rewrite <- comp_assoc, -> delta. ``` ```unfold δ. ``` ```rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l. ``` ```unfold cont at 1. ``` ```rewrite -> prodhom_pair, -> id_r. ``` ```rewrite -> curry2. ``` ```rewrite -> pr2_pair. ``` ```rewrite -> curry_uncurry. ``` ```rewrite <- pair_f. ``` ```rewrite -> pr1_pr2_is_id, -> id_r. ``` ```unfold dist2. ``` ```rewrite -> comp_assoc, <- uncurry2. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 curry2. ``` ```rewrite -> comp_assoc with (g':=inl), -> coprodhom_inl. ``` ```rewrite -> comp_assoc with (g':=inr), -> coprodhom_inr. ``` ```rewrite <-2 comp_assoc with (g':=pr2). ``` ```rewrite <- comp_assoc, -> swap_prodhom. ``` ```rewrite -> comp_assoc, <- uncurry1. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite ->2 curry1. ``` ```rewrite <-2 comp_assoc with (f':=y ×× id), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (g':=id ×× y), -> pr2_prodhom. ``` ```rewrite <-2 comp_assoc with (f':=cont (mapc y) ×× id), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (g':=id ×× cont (mapc y)), -> pr2_prodhom. ``` ```rewrite <-2 comp_assoc with (f':=swapp); unfold swapp. ``` ```rewrite ->2 pr2_pair. ``` ```rewrite ->2 comp_assoc, -> curry_cpr_pr1. ``` ```rewrite <- comp_assoc, -> pr1_pair. ``` ```trivial. ``` ```rewrite -> aux2; clear aux2. ``` ```rewrite <- comp_assoc, <- map_comp. ``` ```rewrite <- comp_assoc, -> comp_assoc with (g':=τ). ``` ```rewrite <- str1. ``` ```rewrite -> pr2_prodhom. ``` ```rewrite -> comp_assoc, -> out_mapc. ``` ```rewrite -> comp_assoc; trivial. ``` ```Qed. ``` ```Theorem proving_str2 : forall ``` ```(x y z : Obj), ``` ``` (ηv ∘ p_assoc1) § ∘ τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) = ``` ``` τv ∘ (id ×× τv) ∘ p_assoc1. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold. ``` ```assert (H_main: τv (x:=(x × y)) (y:=z) (a:=a) (b:=b) ``` ``` = mapc p_assoc2 ∘ (τv ∘ (id ×× τv)) ∘ p_assoc1). ``` ```symmetry. ``` ```apply strength2. ``` ```rewrite ->2 comp_assoc, -> out_mapc. ``` ```rewrite <- comp_assoc with (g':=out), -> comp_assoc with (h':=out), -> strength1. ``` ```rewrite <- comp_assoc with (f':=id ×× τv), -> prodhom_comp, -> id_l. ``` ```rewrite -> strength1. ``` ```rewrite ->3 comp_assoc, -> map_comp. ``` ```rewrite -> coprodhom_comp, -> id_l, -> cont_comp. ``` ```rewrite <- comp_assoc with (g':=τ). ``` ```assert (aux1: map (id ×× (((id ⊕⊕ cont τv) ∘ δ))) ∘ τ ∘ (id ×× (τ ∘ (id ×× out))) ``` ``` = (τ ∘ (id (a:=x) ×× ((map (id ⊕⊕ cont τv) ∘ map δ) ∘ τ) ∘ (id (a:=y) ×× out (x:=z) (a:=a) (b:=b))))). ``` ```rewrite -> map_comp. ``` ```rewrite <- id_l with (f':=id), <-2 comp_assoc. ``` ```rewrite <- prodhom_comp with (h:=map ((id ⊕⊕ cont τv) ∘ δ)). ``` ```rewrite ->2 comp_assoc, <- str_map. ``` ```rewrite -> id_l; trivial. ``` ```rewrite <- aux1; clear aux1. ``` ```rewrite <-6 comp_assoc. ``` ```assert (aux2: map p_assoc1 ∘ τ ∘ (id ×× out) = τ ∘ ((id ×× τ ∘ (id ×× out (x:=z) (a:=a) (b:=b))) ∘ p_assoc1 (a:=x) (b:=y))). ``` ```rewrite -> str2. ``` ```unfold p_assoc1. ``` ```rewrite <- comp_assoc with (g':=id ×× τ), -> prodhom_pair, -> id_r. ``` ```rewrite -> prodhom_pair, -> id_r. ``` ```rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_pair, -> id_r. ``` ```rewrite <- comp_assoc, -> pair_f. ``` ```rewrite <- comp_assoc, -> pr1_prodhom, -> id_r. ``` ```rewrite <- comp_assoc, -> pair_f. ``` ```rewrite <- comp_assoc, -> pr1_prodhom, -> id_r. ``` ```rewrite -> pr2_prodhom. ``` ```trivial. ``` ```rewrite <- aux2; clear aux2. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```rewrite <- comp_assoc with (g':=δ), <-3 comp_assoc with (f':=p_assoc1). ``` ```assert (aux3: (p_assoc1 ⊕⊕ (id ×× ((id ×× τv) ∘ p_assoc1) ^^ id)) ∘ δ ``` ``` = δ ∘ ((id ×× (id ⊕⊕ cont (τv (y:=z) (a:=a) (b:=b))) ∘ δ (a:=a) (b:=b) (y:=z)) ∘ p_assoc1 (a:=x) (b:=y))). ``` ```rewrite -> comp_assoc. ``` ```symmetry. ``` ```rewrite <- id_l with (f':=id). ``` ```rewrite <- prodhom_comp. ``` ```rewrite -> comp_assoc. ``` ```rewrite <- delta. ``` ```rewrite -> prodhom_id. ``` ```rewrite <-2 comp_assoc, <- p_assoc_delta. ``` ```rewrite -> comp_assoc, -> coprodhom_comp, -> id_r. ``` ```rewrite -> cont_comp, -> id_l. ``` ```unfold cont. ``` ```trivial. ``` ```rewrite <- aux3; clear aux3. ``` ```rewrite ->3 comp_assoc, -> coprodhom_comp. ``` ```rewrite -> p_assoc_id2. ``` ```unfold cont. ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```rewrite -> post_comp_comp. ``` ```rewrite -> map_comp. ``` ```rewrite ->3 comp_assoc;trivial. ``` ```rewrite -> H_main. ``` ```rewrite ->2 comp_assoc, -> mapc_comp. ``` ```rewrite -> p_assoc_id1. ``` ```rewrite -> mapc_id, -> id_r. ``` ```trivial. ``` ```Qed. ``` ```Theorem proving_str3 :forall (x y : Obj), ``` ``` τv (x:=x) (y:=y) (a:=a) (b:=b) ∘ (id ×× ηv) = ηv. ``` ```Proof. ``` ```intros. ``` ```symmetry. ``` ```unfold ηv at 1. ``` ```apply out_cong. ``` ```rewrite ->2 comp_assoc; rewrite -> out_tuo_is_id; rewrite -> id_r. ``` ```rewrite -> comp_assoc; rewrite -> strength1. ``` ```assert (aux: τ ∘ ((id ×× out) ∘ (id (a:=x) ×× ηv (a:=a) (b:=b) (x:=y))) = η ∘ (id ×× inl)). ``` ```rewrite -> prodhom_comp; rewrite -> id_l; rewrite -> out_unitcofree. ``` ```rewrite <- id_r with (f':=id) at 1; rewrite <- prodhom_comp with (g:=id); rewrite -> comp_assoc. ``` ```rewrite -> str3. ``` ```trivial. ``` ```rewrite <- comp_assoc with (f':=id ×× ηv); rewrite <- comp_assoc with (g':=τ); rewrite -> aux; clear aux. ``` ```rewrite <- map_unit with (f:=id ×× inl). ``` ```rewrite -> comp_assoc; rewrite <- comp_assoc with (g':=map δ); rewrite -> map_comp. ``` ```unfold δ. ``` ```rewrite <- comp_assoc with (g':=dist2), -> dist2_inl. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```rewrite -> map_comp; rewrite -> coprodhom_inl; rewrite -> id_l. ``` ```rewrite -> map_unit; trivial. ``` ```Qed. ``` ```Theorem proving_str4 : forall x y z (f: x ~> (coext T a b y)), ``` ``` (τv ∘ (id ×× f)) § ∘ τv = τv ∘ (id (a:=z) ×× f §). ``` ```Proof. ``` ```intros. ``` ```set (g:=[f,ηv]). ``` ```assert (H1: id = g § ∘ mapc inr). ``` ```unfold g. ``` ```rewrite -> liftingcofree_mapc. ``` ```rewrite -> cpr_inr. ``` ```rewrite -> proving_kl1. ``` ```trivial. ``` ```assert (H2: f = g ∘ inl). ``` ```unfold g; rewrite -> cpr_inl; trivial. ``` ```assert (H_main: (τv ∘ (id ×× g)) § ∘ τv = τv ∘ (id (a:=z) ×× g §)). ``` ```transitivity (coit ((map δ) ∘ τ ∘ (id (a:=z) ×× [map (id ⊕⊕ cont (mapc inr)) ∘ out ∘ g, η ∘ inr]* ∘ out))). ``` ```apply coit2. ``` ```set (h:=map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out ∘ g). ``` ```assert (aux1: [(map δ) ∘ τ ∘ (id ×× h), η ∘ inr] * ∘ (map δ) = (map δ) ∘ (τ ∘ (id (a:=z) ×× [h, η ∘ inr]))*). ``` ```unfold δ at 2. ``` ```rewrite -> lifting_map. ``` ```rewrite -> comp_assoc. ``` ```rewrite -> cpr_coprodhom. ``` ```rewrite -> id_l. ``` ```rewrite -> map_lifting. ``` ```apply f_equal1. ``` ```assert (aux2: η ∘ δ ∘ (id ×× inr (a:=y)) = ``` ```(η ∘ inr) ∘ (pair (pr1 ∘ pr2) (curry (pair (pr1 ∘ pr1) ``` ```(uncurry (b:=b) (c:=coext T a b (x ⊕ y)) (pr2 (a:=a) ∘ pr2 (a:=z))))))). ``` ```unfold δ. ``` ```rewrite <-2 comp_assoc, -> dist2_inr. ``` ```rewrite -> coprodhom_inr. ``` ```rewrite <- comp_assoc; trivial. ``` ```rewrite <- aux2; clear aux2. ``` ```rewrite <- map_unit. ``` ```rewrite <- str3. ``` ```rewrite <-2 comp_assoc with (f':=id ×× inr). ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```unfold dist2. ``` ```rewrite -> comp_assoc, <- uncurry2. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 curry2. ``` ```rewrite -> comp_assoc, -> cpr_inl. ``` ```rewrite -> comp_assoc, -> cpr_inr. ``` ```apply swapp_switch. ``` ```apply curry_cong. ``` ```rewrite -> curry_uncurry. ``` ```case_distinction. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> curry1. ``` ```rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inl), -> prodhom_comp. ``` ```rewrite -> cpr_inl, -> id_l. ``` ```rewrite -> comp_assoc; trivial. ``` ```rewrite -> cpr_inr. ``` ```rewrite -> curry1. ``` ```rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (f':=swapp), <-2 comp_assoc with (f':=id ×× inr), -> prodhom_comp. ``` ```rewrite -> cpr_inr, -> id_l. ``` ```rewrite -> comp_assoc; trivial. ``` ```rewrite <- comp_assoc with (g':=τ). ``` ```assert (aux3: (τ ∘ (id ×× [h, η ∘ inr])) * ∘ τ ∘ (id ×× out) = τ ∘ (id (a:=z) ×× ([h, η ∘ inr]) * ∘ out)). ``` ```rewrite -> str4. ``` ```rewrite <- comp_assoc. ``` ```rewrite -> prodhom_comp. ``` ```rewrite -> id_l; trivial. ``` ```rewrite <- aux3; clear aux3. ``` ```rewrite ->2 comp_assoc with (h':=map δ). ``` ```rewrite <- aux1; clear aux1. ``` ```unfold h. ``` ```rewrite <- comp_assoc with (h':=map δ). ``` ```assert (aux4: (id ×× (map (id ⊕⊕ cont (mapc inr)))) ∘ (id ×× (out ∘ g)) = id (a:=z) ×× (map (id ⊕⊕ cont (mapc (inr (a:=x)))) ∘ out) ∘ g). ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```rewrite -> comp_assoc; trivial. ``` ```rewrite <- aux4; clear aux4. ``` ```rewrite -> comp_assoc with (h':=τ), <- str_map. ``` ```rewrite ->2 comp_assoc with (h':=map δ), -> map_comp. ``` ```rewrite <- delta. ``` ```rewrite -> prodhom_id. ``` ```rewrite ->4 comp_assoc, -> map_lifting. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```rewrite -> comp_assoc with (g':=η), -> map_unit. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```assert (aux5: (id ⊕⊕ cont ((τv ∘ (id ×× (g ∘ inr))) § ∘ τv)) = (id ⊕⊕ cont ((τv ∘ (id ×× g)) § ∘ τv)) ∘ ((id (a:=(z × y)) ⊕⊕ cont (a:=a) (b:=b) (id (a:=z) ×× mapc inr)))). ``` ```rewrite -> coprodhom_comp, -> id_l, -> cont_comp. ``` ```rewrite <- comp_assoc, -> naturality_τv. ``` ```rewrite -> comp_assoc, -> liftingcofree_mapc. ``` ```rewrite <- comp_assoc, -> prodhom_comp, -> id_l. ``` ```trivial. ``` ```rewrite ->2 comp_assoc. ``` ```rewrite <- aux5; clear aux5. ``` ```symmetry; unfold g at 1; symmetry. ``` ```rewrite -> cpr_inr. ``` ```rewrite -> proving_str3. ``` ```rewrite -> proving_kl1, -> id_r. ``` ```rewrite -> lifting1. ``` ```rewrite <- comp_assoc, -> strength1. ``` ```rewrite ->3 comp_assoc, -> lifting_map. ``` ```rewrite -> cpr_coprodhom, -> id_l. ``` ```rewrite -> comp_assoc, -> strength1. ``` ```rewrite <- comp_assoc with (g':=id ×× out), -> prodhom_comp, -> id_l. ``` ```rewrite -> map_comp. ``` ```rewrite <- comp_assoc with (f':=cont τv), -> cont_comp. ``` ```trivial. ``` ```unfold τv. ``` ```apply fusion. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```rewrite <- comp_assoc with (f':=(id ×× g §)), -> prodhom_comp, -> id_l. ``` ```rewrite -> lifting1. ``` ```rewrite <- prodhom_id. ``` ```rewrite -> delta. ``` ```rewrite <-2 comp_assoc with (g':=τ). ``` ```assert (aux6: id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) * ∘ out = ``` ``` (id ×× ([out ∘ g, η ∘ inr ∘ cont (g §)]) *) ∘ (id (a:=z) ×× out)). ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```trivial. ``` ```rewrite -> aux6; clear aux6. ``` ```assert (aux7: id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) * ∘ out = ``` ``` (id ×× ([(map (id ⊕⊕ cont (mapc inr)) ∘ out) ∘ g, η ∘ inr]) *) ∘ (id (a:=z) ×× out)). ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```trivial. ``` ```rewrite -> aux7; clear aux7. ``` ```rewrite ->2 comp_assoc with (h':=τ), <-2 str4. ``` ```rewrite ->4 comp_assoc; ``` ```apply f_equal2;trivial. ``` ```apply f_equal2;trivial. ``` ```rewrite ->2 map_lifting. ``` ```apply f_equal1. ``` ```rewrite <- map_comp, <- comp_assoc with (h':=map δ). ``` ```apply f_equal2;trivial. ``` ```rewrite -> comp_assoc, -> str_map, <- comp_assoc with (h':=τ). ``` ```apply f_equal2;trivial. ``` ```rewrite -> prodhom_comp, -> id_l. ``` ```apply f_equal2;trivial. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 comp_assoc, -> map_comp. ``` ```rewrite -> coprodhom_comp. ``` ```rewrite -> cont_comp, -> id_l. ``` ```rewrite -> comp_assoc, -> map_unit. ``` ```rewrite <- comp_assoc with (f':=inr), -> coprodhom_inr. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```rewrite <- H1. ``` ```rewrite -> cont_id. ``` ```rewrite -> coprodhom_id. ``` ```rewrite -> map_id, -> id_r. ``` ```trivial. ``` ```rewrite -> H2. ``` ```rewrite <- id_l with (f':=id) at 1. ``` ```rewrite <- prodhom_comp. ``` ```rewrite -> comp_assoc, <- liftingcofree_mapc. ``` ```rewrite <- comp_assoc, <- naturality_τv. ``` ```rewrite -> comp_assoc, -> H_main. ``` ```rewrite <- comp_assoc, -> prodhom_comp, -> id_l. ``` ```rewrite -> liftingcofree_mapc. ``` ```trivial. ``` ```Qed. ``` ```(* --- *) ``` ```Theorem proving_strength_iteration_guarded : forall x y z (f: x ~> coext T a b (y ⊕ x)), ``` ```guarded f -> ``` ``` τv ∘ (id ×× f †') = (mapc dist2 ∘ τv ∘ (id (a:=z) ×× f)) †'. ``` ```Proof. ``` ```intros. ``` ```unfold guarded in H. ``` ```inversion H as [u' H']. ``` ```apply unfolding_guarded2. ``` ```unfold guarded. ``` ```exists (map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ ∘ (id ×× u')). ``` ```rewrite ->5 comp_assoc. ``` ```rewrite ->2 map_comp. ``` ```rewrite -> out_mapc. ``` ```rewrite -> coprodhom_comp, -> id_l, -> id_r. ``` ```rewrite <- comp_assoc with (g':=out), -> strength1. ``` ```rewrite <-2 comp_assoc with (f':=id ×× f), -> prodhom_comp. ``` ```rewrite -> H'. ``` ```rewrite <- prodhom_comp. ``` ```rewrite ->3 comp_assoc; apply f_equal2;trivial. ``` ```rewrite -> comp_assoc, ->2 map_comp. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite -> cont_comp. ``` ```rewrite <- comp_assoc, <- str_map. ``` ```rewrite -> comp_assoc; apply f_equal2;trivial. ``` ```rewrite -> map_comp; apply f_equal1. ``` ```rewrite <- cont_id. ``` ```rewrite <- comp_assoc, <- delta. ``` ```rewrite -> prodhom_id. ``` ```rewrite -> cont_id. ``` ```rewrite -> comp_assoc with (g':=(id ×× inl ⊕⊕ id)), -> coprodhom_comp, -> id_l. ``` ```apply f_equal2;trivial. ``` ```apply f_equal2;trivial. ``` ```apply dist2_inl. ``` ```rewrite <- proving_unfolding at 1. ``` ```rewrite <- id_l with (f':=id) at 1. ``` ```rewrite <- prodhom_comp. ``` ```rewrite -> comp_assoc, <- proving_str4. ``` ```assert (aux: ([ηv, τv ∘ (id ×× f †')]) ∘ dist2 = τv ∘ (id (a:=z) ×× [ηv, f †'])). ``` ```unfold dist2. ``` ```rewrite -> comp_assoc, <- uncurry2. ``` ```rewrite -> f_cpr. ``` ```rewrite ->2 curry2. ``` ```rewrite -> comp_assoc, -> cpr_inl. ``` ```rewrite -> comp_assoc, -> cpr_inr. ``` ```apply swapp_switch. ``` ```apply curry_cong. ``` ```rewrite -> curry_uncurry. ``` ```case_distinction. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> curry1. ``` ```rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (g':=id ×× inl), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp. ``` ```rewrite -> cpr_inl, -> id_l. ``` ```rewrite -> proving_str3. ``` ```trivial. ``` ```rewrite -> cpr_inr. ``` ```rewrite -> curry1. ``` ```rewrite <- comp_assoc with (g':=swapp), -> swap_prodhom. ``` ```rewrite -> comp_assoc with (g':=id ×× inr), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp. ``` ```rewrite -> cpr_inr, -> id_l. ``` ```trivial. ``` ```rewrite <- aux; clear aux. ``` ```rewrite <- liftingcofree_mapc. ``` ```rewrite ->2 comp_assoc. ``` ```trivial. ``` ```Qed. ``` ```Theorem proving_strength_iteration : forall x y (f: x ~> coext T a b (y ⊕ x)), ``` ``` τv ∘ (id ×× f †') = ((ηv ∘ dist2) § ∘ τv ∘ (id (a:=x) ×× f)) †'. ``` ```Proof. ``` ```intros. ``` ```rewrite <- mapc_unfold. ``` ```rewrite -> itercofree_triangle. ``` ```rewrite -> proving_strength_iteration_guarded. ``` ```symmetry; rewrite -> itercofree_triangle; symmetry. ``` ```apply f_equal1. ``` ```unfold triangle. ``` ```rewrite <- id_l with (f':=id). ``` ```rewrite <- comp_assoc with (h':=tuo), <- prodhom_comp, -> id_l, -> comp_assoc. ``` ```assert (bottom_triangle: tuo ∘ map (dist2 ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ ``` ``` = mapc (dist2 (x:=x) (y:=y)) ∘ τv ∘ (id (a:=x) ×× tuo (a:=a) (b:=b))). ``` ```symmetry. ``` ```assert (aux2: τv (x:=x) (y:=(y ⊕ x)) (a:=a) (b:=b) = tuo ∘ map (id ⊕⊕ cont τv) ∘ map δ ∘ τ ∘ (id ×× out)). ``` ```apply out_cong. ``` ```rewrite -> strength1. ``` ```rewrite ->4 comp_assoc with (h':=out). ``` ```rewrite -> out_tuo_is_id, -> id_r. ``` ```trivial. ``` ```rewrite -> aux2 at 1; clear aux2. ``` ```rewrite <-2 comp_assoc with (f':=id ×× tuo), -> prodhom_comp, -> id_r. ``` ```rewrite -> out_tuo_is_id, -> prodhom_id, -> id_l. ``` ```apply out_cong. ``` ```rewrite ->7 comp_assoc. ``` ```rewrite -> out_tuo_is_id, -> id_r. ``` ```rewrite -> out_mapc. ``` ```rewrite <- comp_assoc with (g':=out), -> out_tuo_is_id, -> id_l. ``` ```rewrite -> map_comp. ``` ```rewrite -> coprodhom_comp, -> id_l. ``` ```rewrite -> cont_comp. ``` ```trivial. ``` ```rewrite <- bottom_triangle. ``` ```assert (aux3: (id ×× map (inl ⊕⊕ id)) ∘ (id ×× ((π ∘ out) ∘ f) †) ``` ``` = id (a:=x) ×× map (inl (b:=x) ⊕⊕ id) ∘ ((π ∘ out) ∘ f) †). ``` ```rewrite -> prodhom_comp. ``` ```rewrite -> id_l. ``` ```trivial. ``` ```rewrite <- aux3; clear aux3. ``` ```rewrite -> comp_assoc with (g':=id ×× map (inl ⊕⊕ id)). ``` ```rewrite <-5 comp_assoc with (h':=tuo). ``` ```apply f_equal2; trivial. ``` ```assert (middle_square: map (inl ⊕⊕ id) ∘ map (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ map δ ∘ τ = ``` ``` map (dist2 ⊕⊕ cont (mapc (dist2 (x:=x) (y:=y)) ∘ τv (a:=a) (b:=b))) ∘ map (δ (a:=a) (b:=b)) ∘ τ ∘ (id (a:=x) ×× map (inl (a:=y) (b:=x) ⊕⊕ id))). ``` ```rewrite <- comp_assoc with (g':=τ), <- str_map. ``` ```rewrite <-2 comp_assoc with (g':=map δ). ``` ```rewrite -> comp_assoc with (h':=map δ), -> map_comp with (g:=id ×× (inl ⊕⊕ id)), <-2 cont_id. ``` ```rewrite <- delta. ``` ```rewrite -> prodhom_id. ``` ```rewrite ->2 cont_id. ``` ```rewrite ->2 comp_assoc, ->3 map_comp. ``` ```rewrite -> comp_assoc, ->2 coprodhom_comp, ->2 id_l, -> id_r. ``` ```rewrite -> dist2_inl. ``` ```trivial. ``` ```rewrite <- middle_square. ``` ```rewrite <- comp_assoc with (f':=map δ), -> map_comp. ``` ```set (p:= (id ⊕⊕ cont (mapc dist2 ∘ τv)) ∘ δ). ``` ```rewrite <-2 comp_assoc with (h':=map (inl ⊕⊕ id)). ``` ```apply f_equal2; trivial. ``` ```(* top triangle *) ``` ```rewrite <- comp_assoc, -> strength_iteration. ``` ```rewrite -> map_naturality. ``` ```assert (aux4: (id ×× π) ∘ (id ×× out) ∘ (id ×× f) ``` ``` = id (a:=x) ×× (π ∘ out) ∘ f). ``` ```rewrite ->2 prodhom_comp. ``` ```rewrite ->2 id_l. ``` ```trivial. ``` ```rewrite <- aux4; clear aux4. ``` ```unfold π. ``` ```rewrite <- comp_assoc with (g':=τ), ->2 comp_assoc with (h':=τ), <- str_map. ``` ```rewrite -> comp_assoc, -> map_comp. ``` ```rewrite ->3 comp_assoc, -> map_comp. ``` ```apply f_equal1. ``` ```rewrite <- comp_assoc with (g':=out), ->2 comp_assoc with (h':=out), -> out_mapc. ``` ```rewrite ->3 comp_assoc, -> map_comp. ``` ```apply f_equal2; trivial. ``` ```rewrite <- comp_assoc with (g':=out), -> strength1. ``` ```rewrite -> comp_assoc with (f':=id ×× out);apply f_equal2; trivial. ``` ```rewrite -> comp_assoc with (f':=τ); apply f_equal2; trivial. ``` ```rewrite ->2 map_comp. ``` ```apply f_equal1. ``` ```rewrite <- comp_assoc with (g':=dist2 ⊕⊕ cont (mapc dist2)), -> comp_assoc with (g':=id ⊕⊕ cont τv), ``` ``` -> coprodhom_comp. ``` ```rewrite -> cont_comp, -> id_l. ``` ```rewrite -> comp_assoc, -> cpr_coprodhom. ``` ```unfold δ. ``` ```rewrite -> comp_assoc, -> cpr_coprodhom, -> id_l. ``` ```unfold dist2 at 4. ``` ```rewrite -> comp_assoc, <- uncurry2, -> f_cpr. ``` ```rewrite ->2 curry2. ``` ```rewrite -> comp_assoc, -> cpr_inl. ``` ```rewrite -> comp_assoc, -> cpr_inr. ``` ```symmetry; apply swapp_switch; symmetry. ``` ```apply curry_cong. ``` ```rewrite -> curry_uncurry. ``` ```case_distinction. ``` ```rewrite -> cpr_inl. ``` ```rewrite -> curry1. ``` ```rewrite <- comp_assoc, -> swap_prodhom. ``` ```rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inl), -> prodhom_comp. ``` ```rewrite -> cpr_inl, -> id_l. ``` ```rewrite <- comp_assoc with (g':=dist2), <- naturality_dist2. ``` ```rewrite -> comp_assoc, -> coprodhom_comp. ``` ```rewrite -> prodhom_id, -> id_l. ``` ```apply f_equal1. ``` ```apply f_equal2;trivial. ``` ```apply f_equal2;trivial. ``` ```apply f_equal2;trivial. ``` ```unfold p. ``` ```unfold δ. ``` ```rewrite <-2 comp_assoc. ``` ```rewrite -> dist2_inl. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```rewrite -> coprodhom_inl, -> id_l. ``` ```trivial. ``` ```rewrite -> cpr_inr. ``` ```rewrite -> curry1, <- comp_assoc. ``` ```rewrite -> swap_prodhom. ``` ```rewrite -> comp_assoc with (f':=swapp), <- comp_assoc with (f':=id ×× inr), -> prodhom_comp. ``` ```rewrite -> cpr_inr. ``` ```rewrite <- prodhom_comp. ``` ```rewrite <- comp_assoc with (g':=dist2), -> comp_assoc with (h':=dist2), -> dist2_inl. ``` ```rewrite -> comp_assoc, -> coprodhom_inl. ``` ```apply f_equal1. ``` ```apply f_equal2;trivial. ``` ```rewrite <-3 comp_assoc; apply f_equal2;trivial. ``` ```unfold p. ``` ```unfold δ. ``` ```rewrite ->2 comp_assoc, -> coprodhom_comp, -> id_l. ``` ```rewrite <- comp_assoc, -> dist2_inr. ``` ```rewrite -> coprodhom_inr, -> comp_assoc. ``` ```trivial. ``` ```apply guardedtriangle_def. ``` ```Qed. ``` ```(* incorporate parameters a, b into definitions for the instance declaration; ``` ``` this doesn't change the significance of the proofs established above *) ``` ```Definition ηv' (x : Obj) := ``` ```ηv (x:=x) (a:=a) (b:=b). ``` ```Definition lifting_cofree' (x y : Obj) (f: x ~> coext T a b y) := ``` ```f §. ``` ```Definition iter_cofree' (x y : Obj) (f: x ~> coext T a b (y ⊕ x)) := ``` ```f †'. ``` ```Definition τv' (x y : Obj) := ``` ```τv (x:=x) (y:=y) (a:=a) (b:=b). ``` ```(* Proof that a cofree extension is an ElgotMonad *) ``` ```Instance cofree : ElgotMonad Obj Hom0 C (coext T a b) := { ``` ``` η := ηv'; ``` ``` lifting := lifting_cofree'; ``` ``` iter := iter_cofree'; ``` ``` τ := τv' ``` ```}. ``` ```Proof. ``` ```apply proving_kl1. ``` ```apply proving_kl2. ``` ```apply proving_kl3. ``` ```apply proving_str1. ``` ```apply proving_str2. ``` ```apply proving_str3. ``` ```apply proving_str4. ``` ```apply proving_unfolding. ``` ```apply proving_naturality. ``` ```apply proving_dinaturality. ``` ```apply proving_codiagonal. ``` ```apply proving_uniformity. ``` ```apply proving_strength_iteration. ``` ```Qed. ``` ```(* ``` ```Print Assumptions cofree. ``` ```*) ``` ```End ContextCofreeElgotMonad. ```