Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export functor. Module Nat_Trans. Export Functor. Record data : Type := precreate { nsource : Functor.data; ntarget : Functor.data; osource := fsource nsource; otarget := ftarget ntarget; ntrans : E1 }. Definition create f g t := precreate f g (fun x => Y (ob (fsource f) x) (t x) emptyset). Lemma nsource_create : forall f g t, nsource (create f g t) = f. Proof. ir. tv. Qed. Lemma ntarget_create : forall f g t, ntarget (create f g t) = g. Proof. ir. tv. Qed. Lemma ntrans_create_ob : forall f g t x, ob (fsource f) x -> ntrans (create f g t) x = (t x). Proof. ir. uf create. transitivity (Y (ob (fsource f) x) (t x) emptyset). tv. ap Y_if. am. tv. Qed. Lemma ntrans_create_not_ob : forall f g t x, ~(ob (fsource f) x) -> ntrans (create f g t) x = emptyset. Proof. ir. uf create. transitivity (Y (ob (fsource f) x) (t x) emptyset). tv. ap Y_if_not. am. tv. Qed. Lemma osource_create : forall f g t, osource (create f g t) = fsource f. Proof. ir. uf osource. rw nsource_create; tv. Qed. Lemma otarget_create : forall f g t, otarget (create f g t) = ftarget g. Proof. ir. uf otarget. rw ntarget_create; tv. Qed. Definition like t := create (nsource t) (ntarget t) (ntrans t) = t. Lemma create_like : forall f g t, like (create f g t). Proof. ir. uf like. rw nsource_create. rw ntarget_create. uf create. assert ((fun x : E => Y (ob (fsource f) x) (ntrans (precreate f g (fun x0 : E => Y (ob (fsource f) x0) (t x0) emptyset)) x) emptyset) = (fun x : E => Y (ob (fsource f) x) (t x) emptyset)). ap arrow_extensionality; ir. apply by_cases with (ob (fsource f) a); ir. ap Y_if. am. sy. tv. ap Y_if_not. am. ap Y_if_not; try am. tv. rw H. tv. Qed. Lemma like_extensionality : forall a b, like a -> like b -> nsource a = nsource b -> ntarget a = ntarget b -> (forall x, (ob (osource a) x) -> ntrans a x = ntrans b x) -> a = b. Proof. ir. uh H; uh H0. wr H; wr H0. assert (ntrans a = ntrans b). ap arrow_extensionality. ir. apply by_cases with (ob (osource a) a0); ir. ap H3; am. wr H. rw ntrans_create_not_ob. wr H0. rw ntrans_create_not_ob. tv. wr H1. am. am. rw H1; rw H2; rw H4; tv. Qed. Definition axioms t := (like t) & (Category.axioms (osource t)) & (Category.axioms (otarget t)) & (Functor.axioms (nsource t)) & (Functor.axioms (ntarget t)) & (fsource (ntarget t)) = (osource t) & (ftarget (nsource t)) = (otarget t) & (forall x, ob (osource t) x -> mor (otarget t) (ntrans t x)) & (forall x, ob (osource t) x -> source (ntrans t x) = fob (nsource t) x) & (forall x, ob (osource t) x -> target (ntrans t x) = fob (ntarget t) x) & (forall u, mor (osource t) u -> comp (otarget t) (ntrans t (target u)) (fmor (nsource t) u) =comp (otarget t) (fmor (ntarget t) u) (ntrans t (source u))). Definition property f g t := (Functor.axioms f) & (Functor.axioms g) & (fsource f) = (fsource g) & (ftarget f) = (ftarget g) & (forall x, ob (fsource f) x -> mor (ftarget g) (t x)) & (forall x, ob (fsource f) x -> source (t x) = fob f x) & (forall x, ob (fsource f) x -> target (t x) = fob g x) & (forall u, mor (fsource f) u -> comp (ftarget g) (t (target u)) (fmor f u) = comp (ftarget g) (fmor g u) (t (source u))). Lemma create_axioms : forall f g t, property f g t -> axioms (create f g t). Proof. ir. uf axioms. dj; try (ap create_like); do 3 (first [rw osource_create| rw otarget_create| rw nsource_create| rw ntarget_create| idtac]). lu. lu. lu. lu. uh H; ee. sy; am. lu. uh H; ee. rw ntrans_create_ob. ap H11. rwi osource_create H7. am. rwi osource_create H7. am. rw ntrans_create_ob. rwi osource_create H8. uh H; ee; au. rwi osource_create H8; am. rw ntrans_create_ob. rwi osource_create H9; uh H; ee; au. rwi osource_create H9; am. rw ntrans_create_ob. rw ntrans_create_ob. rwi osource_create H10. uh H; ee; au. rwi mor_facts_rw H10. uh H10; ee; am. rwi mor_facts_rw H10. uh H10; ee; am. Qed. Lemma axioms_property : forall t, axioms t -> property (nsource t) (ntarget t) (ntrans t). Proof. ir. uh H; uhg; xd. Qed. Lemma fsource_ntarget : forall a, axioms a -> fsource (ntarget a) = osource a. Proof. ir. lu. Qed. Lemma ftarget_nsource : forall a, axioms a -> ftarget (nsource a) = otarget a. Proof. ir. lu. Qed. Lemma mor_ntrans : forall a c x, axioms a -> ob (osource a) x -> c = otarget a -> mor c (ntrans a x). Proof. ir. uh H; ee. rw H1; au. Qed. Lemma source_ntrans : forall a x, axioms a -> ob (osource a) x -> source (ntrans a x) = fob (nsource a) x. Proof. ir. uh H; xd. Qed. Lemma target_ntrans : forall a x, axioms a -> ob (osource a) x -> target (ntrans a x) = fob (ntarget a) x. Proof. ir. uh H; xd. Qed. Lemma carre : forall a u, axioms a -> mor (osource a) u -> comp (otarget a) (ntrans a (target u)) (fmor (nsource a) u)= comp (otarget a) (fmor (ntarget a) u) (ntrans a (source u)). Proof. ir. uh H; xd. Qed. Lemma carre_verbose_rw : forall a c1 f u, axioms a -> mor (osource a) u -> c1 = otarget a -> f = nsource a -> comp c1 (ntrans a (target u)) (fmor f u)= comp (otarget a) (fmor (ntarget a) u) (ntrans a (source u)). Proof. ir. rw H1; rw H2. ap carre; am. Qed. Definition globular_facts a := fsource (nsource a) = osource a & fsource (ntarget a) = osource a & ftarget (nsource a) = otarget a & ftarget (ntarget a) = otarget a. Lemma axioms_globular : forall a, axioms a -> globular_facts a. Proof. ir. uhg; ee; lu. Qed. Definition vident f := create f f (fun x => id (ftarget f) (fob f x)). Lemma nsource_vident : forall f, nsource (vident f) = f. Proof. ir. tv. Qed. Lemma ntarget_vident : forall f, ntarget (vident f) = f. Proof. ir. tv. Qed. Lemma osource_vident : forall f, osource (vident f) = (fsource f). Proof. ir. tv. Qed. Lemma otarget_vident : forall f, otarget (vident f) = (ftarget f). Proof. ir. tv. Qed. Lemma ntrans_vident : forall f x, ob (fsource f) x -> ntrans (vident f) x = id (ftarget f) (fob f x). Proof. ir. uf vident. rw ntrans_create_ob. tv. am. Qed. Definition vcompose a b := create (nsource b) (ntarget a) (fun x => comp (otarget a) (ntrans a x) (ntrans b x)). Lemma nsource_vcompose : forall a b, nsource (vcompose a b) = (nsource b). Proof. ir. tv. Qed. Lemma ntarget_vcompose : forall a b, ntarget (vcompose a b) = (ntarget a). Proof. ir. tv. Qed. Lemma osource_vcompose : forall a b, osource (vcompose a b) = osource b. Proof. ir. tv. Qed. Lemma otarget_vcompose : forall a b, otarget (vcompose a b) = otarget a. Proof. ir. tv. Qed. Lemma ntrans_vcompose : forall a b x, ob (osource b) x -> ntrans (vcompose a b) x = comp (otarget a) (ntrans a x) (ntrans b x). Proof. ir. uf vcompose. rw ntrans_create_ob. tv. am. Qed. Lemma vcompose_axioms : forall a b, axioms a -> axioms b -> nsource a = ntarget b -> axioms (vcompose a b). Proof. ir. uf vcompose; ap create_axioms. cp (axioms_globular H). cp (axioms_globular H0). uh H2; uh H3; ee. assert (lem1 : osource a = osource b). uf osource. rw H1. rw H4. am. assert (lem2 : otarget a = otarget b). uf otarget. wr H1. rw H8. tv. assert (lem3 : forall x, ob (osource b) x -> composable (otarget a) (ntrans a x) (ntrans b x)). ir. ap show_composable. ap mor_ntrans; try am. rw lem1; am. ap mor_ntrans; try am. rw source_ntrans. rw target_ntrans. rw H1; tv. am. am. am. rw lem1; am. tv. uhg; dj. lu. lu. rw H7. sy; am. rw H5. sy; am. ap mor_comp. ap lem3; am. rw source_comp. rw source_ntrans. tv. am. am. ap lem3; am. rw target_comp. rw target_ntrans; try tv; try am. rw lem1; am. ap lem3; am. cp H17. rwi mor_facts_rw H18. uh H18; ee. transitivity (comp (otarget a) (ntrans a (target u)) (comp (otarget a) (ntrans b (target u)) (fmor (nsource b) u))). ap verbose_assoc. ap lem3; try am. ap show_composable; try am. ap mor_ntrans; try am. rw lem2. wr H5. ap mor_fmor. lu. am. rw source_ntrans; try am. rw target_fmor. tv. lu. am. rw lem2. am. tv. tv. tv. tv. tv. rw carre_verbose_rw. wr assoc. wr lem2. wr assoc. uf otarget. ap uncomp. tv. wr H1. rw H9. rw carre_verbose_rw. ap uneq. tv. (*** the rest is discharging obligations from the lemmas and rewriting applied above ***) am. rw lem1; am. tv. tv. tv. tv. ap show_composable. ap mor_ntrans. am. rw lem1. am. tv. rw lem2. uf otarget; ap mor_fmor; try am. lu. rw H4. am. rw source_ntrans. uf otarget; rw target_fmor. rw H1. tv. lu. rw H4; am. am. rw lem1; am. tv. ap show_composable. rw lem2. uf otarget; ap mor_fmor. lu. rw H4; am. rw lem2. ap mor_ntrans. am. am. tv. uf otarget; rw source_fmor. rw target_ntrans. ap uneq. tv. am. am. tv. lu. rw H4; am. ap show_composable. uf otarget. ap mor_fmor. lu. rw H7. rw lem1; am. ap mor_ntrans. am. rw lem1; am. tv. uf otarget; rw source_fmor. rw target_ntrans. ap uneq. tv. am. rw lem1; am. tv. rw H7. rw lem1; am. ap show_composable. ap mor_ntrans. am. rw lem1. am. tv. rw lem2. ap mor_ntrans. am. am. tv. rw source_ntrans. rw target_ntrans. rw H1. ap uneq. tv. am. am. am. rw lem1; am. tv. am. am. tv. Qed. Lemma vident_axioms : forall f, Functor.axioms f -> axioms (vident f). Proof. ir. uf vident. ap create_axioms. uhg; dj. am. am. tv. tv. ap mor_id. ap ob_fob. am. am. rw source_id. tv. ap ob_fob; am. rw target_id; try tv; try (ap ob_fob; am). cp H7; rwi mor_facts_rw H7; uh H7; ee. rw left_id. rw right_id. tv. ap ob_fob; am. ap mor_fmor; am. rw source_fmor; try am. tv. ap ob_fob; try am. ap mor_fmor; am. rw target_fmor; try am. tv. Qed. Lemma axioms_extensionality : forall a b, axioms a -> axioms b -> nsource a = nsource b -> ntarget a = ntarget b -> (forall x, ob (osource a) x -> ntrans a x = ntrans b x) -> a = b. Proof. ir. ap like_extensionality. lu. lu. am. am. am. Qed. Lemma left_vident : forall a, axioms a -> vcompose (vident (ntarget a)) a = a. Proof. ir. ap axioms_extensionality. ap vcompose_axioms. ap vident_axioms. lu. am. rw nsource_vident; tv. am. rw nsource_vcompose. tv. rw ntarget_vcompose. rw ntarget_vident. tv. ir. cp H0. rwi osource_vcompose H1. cp (axioms_globular H). uh H2; ee. rw ntrans_vcompose. rw ntrans_vident. rw left_id. tv. ap ob_fob. lu. rw H3. am. ap mor_ntrans. am. am. tv. rw target_ntrans. tv. am. am. rw H3. am. am. Qed. Lemma right_vident : forall a, axioms a -> vcompose a (vident (nsource a)) = a. Proof. ir. ap axioms_extensionality. ap vcompose_axioms. am. ap vident_axioms. lu. rw ntarget_vident; tv. am. rw nsource_vcompose. tv. rw ntarget_vcompose. tv. ir. cp H0. rwi osource_vcompose H1. rwi osource_vident H1. cp (axioms_globular H). uh H2; ee. rwi H2 H1. rw ntrans_vcompose. rw ntrans_vident. rw H4. rw right_id. tv. wr H4. ap ob_fob. lu. am. ap mor_ntrans. am. am. tv. rw source_ntrans. tv. am. am. am. am. Qed. Lemma weak_left_vident : forall a f, axioms a -> f = ntarget a -> vcompose (vident f) a = a. Proof. ir. rw H0. ap left_vident. am. Qed. Lemma weak_right_vident : forall a f, axioms a -> f = nsource a -> vcompose a (vident f) = a. Proof. ir. rw H0. ap right_vident. am. Qed. Definition vcomposable a b := axioms a & axioms b & nsource a = ntarget b. Lemma vcomposable_facts : forall a b, vcomposable a b -> (axioms a & axioms b & globular_facts a & globular_facts b & nsource a = ntarget b & osource a = osource b & otarget a = otarget b & (forall x, ob (osource b) x -> composable (otarget a) (ntrans a x) (ntrans b x))). Proof. ir. uh H; dj; ee; try am. ap axioms_globular; am. ap axioms_globular; am. uh H2; ee. uh H3; ee. uf osource. rw H4. rw H10; tv. uf otarget. wr H4. uh H2; ee. rw H9; tv. ap show_composable. ap mor_ntrans. am. rw H5; am. tv. ap mor_ntrans. am. am. am. rw source_ntrans. rw target_ntrans. rw H9; tv. am. am. am. rw H5; am. Qed. Lemma vcompose_assoc : forall a b c, vcomposable a b -> vcomposable b c -> vcompose (vcompose a b) c = vcompose a (vcompose b c). Proof. ir. cp (vcomposable_facts H); cp (vcomposable_facts H0); ee. ap axioms_extensionality; try am. ap vcompose_axioms; try am. ap vcompose_axioms; try am. ap vcompose_axioms; try am. ap vcompose_axioms; try am. rw nsource_vcompose. rw nsource_vcompose. rw nsource_vcompose. tv. rw ntarget_vcompose. rw ntarget_vcompose. rw ntarget_vcompose. tv. ir. rwi osource_vcompose H17. rw ntrans_vcompose. rw ntrans_vcompose. rw ntrans_vcompose. rw ntrans_vcompose. ap verbose_assoc. ap H16. rw H7; am. ap H9. am. rw otarget_vcompose. tv. tv. am. tv. tv. tv. am. rw osource_vcompose. am. rw H7; am. am. Qed. Definition htrans_left f a := create (Functor.compose f (nsource a)) (Functor.compose f (ntarget a)) (fun x => (fmor f (ntrans a x))). Definition htrans_right a f := create (Functor.compose (nsource a) f) (Functor.compose (ntarget a) f) (fun x=> (ntrans a (fob f x))). Lemma nsource_htrans_left : forall f a, nsource (htrans_left f a) = Functor.compose f (nsource a). Proof. ir. tv. Qed. Lemma ntarget_htrans_left : forall f a, ntarget (htrans_left f a) = Functor.compose f (ntarget a). Proof. ir. tv. Qed. Lemma osource_htrans_left : forall f a, osource (htrans_left f a) = osource a. Proof. ir. tv. Qed. Lemma otarget_htrans_left : forall f a, otarget (htrans_left f a) = ftarget f. Proof. ir. tv. Qed. Lemma nsource_htrans_right : forall f a, nsource (htrans_right a f) = Functor.compose (nsource a) f. Proof. ir. tv. Qed. Lemma ntarget_htrans_right : forall f a, ntarget (htrans_right a f) = Functor.compose (ntarget a) f. Proof. ir. tv. Qed. Lemma osource_htrans_right : forall f a, osource (htrans_right a f) = fsource f. Proof. ir. tv. Qed. Lemma otarget_htrans_right : forall f a, otarget (htrans_right a f) = otarget a. Proof. ir. tv. Qed. Lemma ntrans_htrans_left : forall f a x, ob (osource a) x -> ntrans (htrans_left f a) x = fmor f (ntrans a x). Proof. ir. uf htrans_left. rw ntrans_create_ob. tv. am. Qed. Lemma ntrans_htrans_right : forall f a x, ob (fsource f) x -> ntrans (htrans_right a f) x = ntrans a (fob f x). Proof. ir. uf htrans_right. rw ntrans_create_ob. tv. rw fsource_compose. am. Qed. Lemma htrans_left_axioms : forall f a, Functor.axioms f -> axioms a -> fsource f = otarget a -> axioms (htrans_left f a). Proof. ir. cp (axioms_globular H0). uh H2; ee. uf htrans_left. ap create_axioms. uhg; ee; try am. ap Functor.compose_axioms. uhg; ee; try lu. rw H4; am. ap Functor.compose_axioms. uhg; ee; try lu. rw fsource_compose. rw fsource_compose. sy; am. rw ftarget_compose. rw ftarget_compose. tv. ir. rw ftarget_compose. ap mor_fmor. am. rw H1. ap mor_ntrans. am. rwi fsource_compose H6. am. tv. ir. rwi fsource_compose H6. rwi H2 H6. rw fob_compose. rw source_fmor. ap uneq. rw source_ntrans. tv. am. am. tv. rw H1. ap mor_ntrans. am. am. tv. ir. rwi fsource_compose H6. rwi H2 H6. rw target_fmor. rw fob_compose. ap uneq. rw target_ntrans. tv. am. am. tv. rw H1. ap mor_ntrans. am. am. tv. ir. rw ftarget_compose. rw fmor_compose. rw fmor_compose. rw comp_fmor. rw comp_fmor. ap uneq. rw carre_verbose_rw. rw H1. tv. am. rwi fsource_compose H6. am. am. tv. tv. rwi fsource_compose H6. rwi H2 H6. ap show_composable. rw H1. wr H5. ap mor_fmor. lu. rw H3; am. rw H1. ap mor_ntrans. am. rwi mor_facts_rw H6; lu. tv. rw source_fmor. rw target_ntrans. tv. am. rwi mor_facts_rw H6; lu. tv. lu. rw H3; am. am. ap show_composable. rw H1. ap mor_ntrans. am. rwi mor_facts_rw H6; lu. tv. rw H1. wr H4. ap mor_fmor. lu. rwi fsource_compose H6. am. rw source_ntrans. rw target_fmor. tv. lu. rwi fsource_compose H6; am. am. rwi fsource_compose H6. rwi H2 H6. rwi mor_facts_rw H6; lu. Qed. Lemma htrans_right_axioms : forall f a, Functor.axioms f -> axioms a -> osource a = ftarget f -> axioms (htrans_right a f). Proof. ir. cp (axioms_globular H0). uh H2; ee. uf htrans_right. ap create_axioms. uhg; ee; try am. ap Functor.compose_axioms. uhg; ee; try lu. ap Functor.compose_axioms. uhg; ee; try lu. rw H3; am. rw fsource_compose. rw fsource_compose. tv. ir. rw ftarget_compose. rw H5. ap mor_ntrans. am. rw H1. ap ob_fob. am. rwi fsource_compose H6. am. tv. ir. rwi fsource_compose H6. rw source_ntrans. rw fob_compose. tv. am. rw H1. ap ob_fob. am. am. tv. ir. rwi fsource_compose H6. rw target_ntrans. rw fob_compose. tv. am. rw H1. ap ob_fob. am. am. tv. ir. rw ftarget_compose. rw fmor_compose. rw fmor_compose. assert (lem1 : fob f (target u) = target (fmor f u)). rw target_fmor. tv. am. rwi fsource_compose H6. am. rw lem1. rw carre_verbose_rw. ap uneq. ap uneq. rw source_fmor. tv. am. rwi fsource_compose H6; am. am. rwi fsource_compose H6. rw H1. ap mor_fmor. am. am. am. tv. Qed. Definition hcomposable a b := axioms a & axioms b & osource a = otarget b. Definition hcompose a b := vcompose (htrans_right a (ntarget b)) (htrans_left (nsource a) b). Lemma hcompose_axioms : forall a b, hcomposable a b -> axioms (hcompose a b). Proof. ir. uh H; ee. uf hcompose. ap vcompose_axioms. ap htrans_right_axioms. lu. am. rw H1. tv. ap htrans_left_axioms. lu. am. am. rw nsource_htrans_right. rw ntarget_htrans_left. tv. Qed. Lemma nsource_hcompose : forall a b, nsource (hcompose a b) = compose (nsource a) (nsource b). Proof. ir. uf hcompose. rw nsource_vcompose. rw nsource_htrans_left. tv. Qed. Lemma ntarget_hcompose : forall a b, ntarget (hcompose a b) = compose (ntarget a) (ntarget b). Proof. ir. uf hcompose. rw ntarget_vcompose. rw ntarget_htrans_right. tv. Qed. Lemma osource_hcompose : forall a b, osource (hcompose a b) = osource b. Proof. ir. tv. Qed. Lemma otarget_hcompose : forall a b, otarget (hcompose a b) = otarget a. Proof. ir. tv. Qed. Lemma ntrans_hcompose : forall a b x, hcomposable a b -> ob (osource b) x -> ntrans (hcompose a b) x = comp (otarget a) (ntrans a (fob (ntarget b) x)) (fmor (nsource a) (ntrans b x)). Proof. ir. uf hcompose. rw ntrans_vcompose. rw otarget_htrans_right. rw ntrans_htrans_right. rw ntrans_htrans_left. tv. am. uh H; ee. cp (axioms_globular H1). uh H3; ee. rw H4. am. rw osource_htrans_left. am. Qed. Definition hcompose1 a b := vcompose (htrans_left (ntarget a) b) (htrans_right a (nsource b)). Lemma hcompose1_axioms : forall a b, hcomposable a b -> axioms (hcompose1 a b). Proof. ir. uh H; ee. uf hcompose1. ap vcompose_axioms. ap htrans_left_axioms. lu. am. cp (axioms_globular H). uh H2; ee. rw H3. am. ap htrans_right_axioms. lu. am. cp (axioms_globular H0). uh H2; ee. rw H4. am. rw nsource_htrans_left. rw ntarget_htrans_right. tv. Qed. Lemma hcomposable_commutativity : forall a b x, hcomposable a b -> ob (osource b) x -> comp (otarget a) (ntrans a (fob (ntarget b) x)) (fmor (nsource a) (ntrans b x)) = comp (otarget a) (fmor (ntarget a) (ntrans b x)) (ntrans a (fob (nsource b) x)). Proof. ir. cp H. uh H; ee. cp (axioms_globular H). cp (axioms_globular H2). uh H4; uh H5; ee. assert (lem1 : fob (ntarget b) x = target (ntrans b x)). rw target_ntrans. tv. am. am. assert (lem2 : fob (nsource b) x = source (ntrans b x)). rw source_ntrans. tv. am. am. rw lem1. rw carre. rw lem2. tv. am. ap mor_ntrans. am. am. am. Qed. Lemma hcompose_other : forall a b, hcomposable a b -> hcompose a b = hcompose1 a b. Proof. ir. cp H; uh H; ee. assert (lem1: axioms (hcompose a b)). ap hcompose_axioms; am. assert (lem2 : axioms (hcompose1 a b)). ap hcompose1_axioms; am. ap like_extensionality. lu. lu. rw nsource_hcompose. uf hcompose1. rw nsource_vcompose. tv. rw ntarget_hcompose. uf hcompose1. rw ntarget_vcompose. tv. ir. rwi osource_hcompose H3. rw ntrans_hcompose. uf hcompose1. rw ntrans_vcompose. rw otarget_htrans_left. rw ntrans_htrans_left. rw ntrans_htrans_right. assert (ftarget (ntarget a) = otarget a). tv. rw H4. ap hcomposable_commutativity. am. am. am. am. rw osource_htrans_right. am. am. am. Qed. Lemma fsource_nsource : forall a, fsource (nsource a) = osource a. Proof. ir. tv. Qed. Lemma ftarget_ntarget : forall a, ftarget (ntarget a) = otarget a. Proof. ir. tv. Qed. Lemma hcompose_vident_left : forall f a, axioms a -> Functor.axioms f -> fsource f = otarget a -> hcompose (vident f) a = htrans_left f a. Proof. ir. ap axioms_extensionality. ap hcompose_axioms. uhg; ee. ap vident_axioms. am. am. rw osource_vident. am. ap htrans_left_axioms. am. am. am. rw nsource_hcompose. rw nsource_htrans_left. rw nsource_vident. tv. rw ntarget_hcompose. rw ntarget_vident. rw ntarget_htrans_left. tv. ir. rw ntrans_hcompose. rw ntrans_htrans_left. rw otarget_vident. rw ntrans_vident. rw left_id. rw nsource_vident. tv. ap ob_fob. am. rw H1. uf otarget. ap ob_fob. lu. rwi osource_hcompose H2. cp (axioms_globular H). uh H3; ee. rw H4. am. rw nsource_vident. ap mor_fmor. am. rw H1. ap mor_ntrans. am. rwi osource_hcompose H2. am. tv. rw nsource_vident. rw target_fmor. ap uneq. rw target_ntrans. tv. am. rwi osource_hcompose H2. am. tv. rw H1. ap mor_ntrans. am. rwi osource_hcompose H2. am. tv. rw H1. uf otarget. ap ob_fob. lu. rwi osource_hcompose H2. rw fsource_ntarget. am. am. rwi osource_hcompose H2. am. uhg; ee. ap vident_axioms. am. am. rw osource_vident. am. rwi osource_hcompose H2. am. Qed. Lemma hcompose_vident_right : forall a f, axioms a -> Functor.axioms f -> ftarget f = osource a -> hcompose a (vident f) = htrans_right a f. Proof. ir. ap axioms_extensionality. ap hcompose_axioms. uhg; ee; try lu. ap vident_axioms; am. sy; am. ap htrans_right_axioms. am. am. sy; am. tv. tv. ir. rwi osource_hcompose H2. rwi osource_vident H2. rw ntrans_hcompose. rw ntarget_vident. rw ntrans_vident. rw ntrans_htrans_right. rw H1. uf osource. wr id_fob. rw ftarget_nsource. rw right_id. tv. wr ftarget_nsource. ap ob_fob. lu. rw fsource_nsource. wr H1. ap ob_fob; try lu. am. ap mor_ntrans. am. wr H1. ap ob_fob; am. tv. rw source_ntrans. tv. am. wr H1; ap ob_fob; am. tv. lu. rw fsource_nsource; wr H1; ap ob_fob; am. am. am. uhg; ee; try lu. ap vident_axioms; am. rw otarget_vident. sy; am. am. Qed. Lemma vident_hcomposable : forall f g, fcomposable f g -> hcomposable (vident f) (vident g). Proof. ir. uhg; ee. ap vident_axioms; lu. ap vident_axioms; lu. lu. Qed. Lemma hcompose_vident_vident : forall f g, fcomposable f g -> hcompose (vident f) (vident g) = vident (compose f g). Proof. ir. rw hcompose_vident_left. ap axioms_extensionality. ap htrans_left_axioms. lu. ap vident_axioms; lu. lu. ap vident_axioms. ap Functor.compose_axioms. am. tv. tv. ir. rwi osource_htrans_left H0. rwi osource_vident H0. rw ntrans_htrans_left. rw ntrans_vident. rw ntrans_vident. rw fob_compose. uh H; ee. wr H2. wr id_fob. tv. am. rw H2. ap ob_fob; am. am. am. am. ap vident_axioms. lu. lu. lu. Qed. Lemma htrans_right_vident : forall f g, fcomposable f g -> htrans_right (vident f) g = vident (compose f g). Proof. ir. wr hcompose_vident_right. rw hcompose_vident_vident. tv. am. ap vident_axioms. lu. lu. rw osource_vident. uh H; ee. sy; am. Qed. Lemma htrans_left_vident : forall f g, fcomposable f g -> htrans_left f (vident g) = vident (compose f g). Proof. ir. wr hcompose_vident_left. rw hcompose_vident_vident. tv. am. ap vident_axioms. lu. lu. rw otarget_vident. uh H; ee. am. Qed. Lemma interchange : forall a b c d, ntarget a = nsource c -> ntarget b = nsource d -> osource b = otarget a -> axioms a -> axioms b -> axioms c -> axioms d -> vcompose (hcompose d c) (hcompose b a) = hcompose (vcompose d b) (vcompose c a). Proof. ir. assert (lema : osource d = otarget c). uf osource. wr ftarget_nsource. wr H0. wr H. rw fsource_ntarget. am. am. am. assert (lemb : osource d = osource b). rw lema. wr fsource_ntarget. rw H0. sy; am. am. assert (lem1 : hcomposable d c). uhg; ee; try am. assert (lem2 : hcomposable b a). uhg; ee; try am. assert (lem3 : vcomposable d b). uhg; ee; try am. sy; am. assert (lem4 : vcomposable c a). uhg; ee; try am. sy; am. assert (lem5: otarget d = otarget b). uf otarget. rw H0. rw ftarget_nsource. tv. am. assert (lem6 : osource c = osource a). uf osource. wr H. rw fsource_ntarget. tv. am. assert (lem7 : otarget d = otarget b). uf otarget. rw H0. rw ftarget_nsource. tv. am. assert (lem8 : osource b = otarget c). wr lema. sy; am. ap axioms_extensionality. ap vcompose_axioms. ap hcompose_axioms; am. ap hcompose_axioms; am. rw nsource_hcompose. rw ntarget_hcompose. rw H0. rw H. tv. ap hcompose_axioms. uhg; ee. ap vcompose_axioms. am. am. sy; am. ap vcompose_axioms; try am. sy; am. rw osource_vcompose. rw otarget_vcompose. rw H1. wr lema. rw lemb. sy; am. tv. tv. ir. rwi osource_vcompose H6. rwi osource_hcompose H6. assert (obc : ob (osource c) x). rw lem6; am. rw ntrans_vcompose; try am. rw ntrans_hcompose; try am. rw ntrans_hcompose; try am. rw ntrans_hcompose; try am. rw ntrans_vcompose; try am. rw otarget_hcompose. rw otarget_vcompose. rw nsource_vcompose. rw ntrans_vcompose. rw ntarget_vcompose. rw assoc_verbose_rw. rw assoc_verbose_rw. ap uneq. wr assoc_verbose_rw. sy. wr lema. rw lemb. uf osource. wr comp_fmor. wr assoc_verbose_rw. rw ftarget_nsource. ap uncomp. tv. rw H. wr H0. rw lem5. ap hcomposable_commutativity. uhg; ee; try am. am. (*** discharge of rewriting obligations ***) uf osource. tv. am. ap show_composable. rw lem5. ap mor_ntrans. am. wr lemb. rw lema. uf otarget. ap ob_fob. lu. rw fsource_ntarget. uf osource. wr H. rw fsource_ntarget. am. am. am. tv. rw lem7. wr ftarget_nsource. ap mor_fmor. lu. rw fsource_nsource. wr lemb. rw lema. ap mor_ntrans. am. rw lem6; am. tv. am. rw source_ntrans. rw target_fmor. ap uneq. rw target_ntrans. tv. am. rw lem6; am. tv. lu. rw fsource_nsource. wr lemb. rw lema. ap mor_ntrans. am. rw lem6; am. tv. am. wr lemb. rw lema. uf otarget. ap ob_fob. lu. rw fsource_ntarget. rw lem6. am. am. tv. ap show_composable. ap mor_fmorv. lu. ap mor_ntrans; try am. tv. ap mor_fmorv. lu. ap mor_ntrans; try am. tv. rw source_fmor. rw target_fmor. ap uneq. rw source_ntrans. rw target_ntrans. wr H; tv. am. am. am. am. lu. ap mor_ntrans. am. am. am. lu. ap mor_ntrans. am. am. am. rw ftarget_nsource. sy; am. am. lu. ap show_composable. ap mor_ntrans; try am. ap mor_ntrans; try tv; try am. rw source_ntrans. rw target_ntrans. rw H. tv. am. am. am. am. ap show_composable. ap mor_fmorv. lu. ap mor_ntrans. am. am. am. rw ftarget_nsource; tv. ap mor_ntrans. am. ap ob_fobv. lu. rw fsource_ntarget. am. am. am. am. rw target_ntrans. wr H0. rw source_fmor. ap uneq. rw H. rw source_ntrans. tv. am. am. lu. ap mor_ntrans. am. am. rw fsource_ntarget. wr lemb; rw lema; tv. am. am. ap ob_fobv. lu. rw fsource_ntarget. am. am. am. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_fmorv. lu. app mor_ntrans. rww ftarget_nsource. rww source_ntrans. rww target_fmor. ap uneq. rww target_ntrans. lu. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. sy; am. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. rww source_ntrans. rww target_ntrans. wr H0. ap uneq. tv. app ob_fobv. lu. rww fsource_ntarget. app ob_fobv. lu. rww fsource_ntarget. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_fmorv. lu. app mor_compv. app show_composable. app mor_ntrans. app mor_ntrans. rww target_ntrans. rww source_ntrans. rww H. rww ftarget_nsource. rww source_ntrans. rww target_fmor. rww target_comp. rww target_ntrans. app show_composable. app mor_ntrans. app mor_ntrans. wr H1; wr lemb; rw lema; tv. rw source_ntrans. rw target_ntrans. rw H; tv. am. am. am. am. lu. app mor_compv. app show_composable. app mor_ntrans. app mor_ntrans. rww target_ntrans. rww source_ntrans. rww H. app ob_fobv. lu. rww fsource_ntarget. tv. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_fmorv. lu. app mor_ntrans. rww ftarget_nsource. rww source_ntrans. rww target_fmor. rww target_ntrans. lu. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app show_composable. app mor_fmorv. lu. app mor_ntrans. rww ftarget_nsource. app mor_compv. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_fmorv. lu. app mor_ntrans. rww ftarget_nsource. rww source_ntrans. rww target_fmor. rww target_ntrans. lu. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. rww target_comp. rww target_ntrans. rww source_fmor. rww source_ntrans. wrr H0. ap uneq. rww H. lu. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app show_composable. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. app mor_fmorv. lu. app mor_ntrans. rww ftarget_nsource. rww source_ntrans. rww target_fmor. rww target_ntrans. lu. app mor_ntrans. app ob_fobv. lu. rww fsource_ntarget. lu. lu. app ob_fobv. lu. rww fsource_ntarget. app vcompose_axioms. lu. uhg; ee. app vcompose_axioms. lu. app vcompose_axioms. sy; am. rww osource_vcompose. Qed. End Nat_Trans. Module Constant_Nat_Trans. Export Constant_Functor. Export Nat_Trans. Definition constant_nt a b u := create (constant_functor a b (source u)) (constant_functor a b (target u)) (fun x:E => u). Lemma osource_constant_nt : forall a b u, osource (constant_nt a b u) = a. Proof. ir. tv. Qed. Lemma otarget_constant_nt : forall a b u, otarget (constant_nt a b u) = b. Proof. ir. tv. Qed. Lemma nsource_constant_nt : forall a b u, nsource (constant_nt a b u) = constant_functor a b (source u). Proof. ir. tv. Qed. Lemma ntarget_constant_nt : forall a b u, ntarget (constant_nt a b u) = constant_functor a b (target u). Proof. ir. tv. Qed. Lemma ntrans_constant_nt : forall a b u x, ob a x -> ntrans (constant_nt a b u) x = u. Proof. ir. uf constant_nt. rw ntrans_create_ob. tv. am. Qed. Lemma constant_nt_axioms : forall a b u, Category.axioms a -> Category.axioms b -> mor b u -> axioms (constant_nt a b u). Proof. ir. uf constant_nt. ap create_axioms. cp H1. rwi mor_facts_rw H2. uh H2; ee. uhg; ee. app constant_functor_axioms. app constant_functor_axioms. rww fsource_constant_functor. rww ftarget_constant_functor. ir. rww ftarget_constant_functor. ir. rww fob_constant_functor. ir. rww fob_constant_functor. ir. rww fmor_constant_functor. rww fmor_constant_functor. rww left_id. Qed. End Constant_Nat_Trans.