Set Implicit Arguments. Unset Strict Implicit. Require Import Arith. Require Export nat_trans. Module Limit. Export Constant_Nat_Trans. Definition vertex a := constant_value (nsource a). Definition is_cone a := Nat_Trans.axioms a & is_constant (nsource a) & ob (otarget a) (vertex a). Lemma cone_source_ntrans : forall a x, is_cone a -> ob (osource a) x -> source (ntrans a x) = (vertex a). Proof. ir. rw source_ntrans. uh H; ee. uh H1; ee. rw H1. rw fob_constant_functor. tv. lu. am. Qed. Definition cone_composable a u := is_cone a & mor (otarget a) u & target u = vertex a. Definition cone_compose a u := vcompose a (constant_nt (osource a) (otarget a) u). Lemma nsource_cone_compose : forall a u, nsource (cone_compose a u) = constant_functor (osource a) (otarget a) (source u). Proof. ir. uf cone_compose. rw nsource_vcompose. rw nsource_constant_nt. tv. Qed. Lemma vertex_cone_compose : forall a u, vertex (cone_compose a u) = source u. Proof. ir. uf vertex. rw nsource_cone_compose. uf constant_value. tv. Qed. Lemma ntarget_cone_compose : forall a u, ntarget (cone_compose a u) = ntarget a. Proof. ir. uf cone_compose. rw ntarget_vcompose. tv. Qed. Lemma osource_cone_compose : forall a u, osource (cone_compose a u) = osource a. Proof. ir. tv. Qed. Lemma otarget_cone_compose : forall a u, otarget (cone_compose a u) = otarget a. Proof. ir. tv. Qed. Lemma ntrans_cone_compose : forall a u x, ob (osource a) x -> ntrans (cone_compose a u) x = comp (otarget a) (ntrans a x) u. Proof. ir. uf cone_compose. rw ntrans_vcompose. rw ntrans_constant_nt. tv. am. am. Qed. Lemma is_cone_cone_compose : forall a u, cone_composable a u -> is_cone (cone_compose a u). Proof. ir. uhg; ee. uf cone_compose. ap vcompose_axioms. lu. ap constant_nt_axioms. lu. lu. lu. rw ntarget_constant_nt. uh H; ee. uh H; ee. uh H2. rwi fsource_nsource H2. rwi ftarget_nsource H2. rw H1. exact H2. am. rw nsource_cone_compose. ap constant_functor_is_constant. lu. uh H; ee. rwi mor_facts_rw H0; lu. rw otarget_cone_compose. uh H; ee. uf vertex. rw nsource_cone_compose. uf constant_value. rw fob_constant_functor. rwi mor_facts_rw H0; lu. Qed. Lemma cone_compose_axioms : forall a u, cone_composable a u -> Nat_Trans.axioms (cone_compose a u). Proof. ir. cp (is_cone_cone_compose H). lu. Qed. Lemma cone_compose_cone_compose : forall a u v, cone_composable a u -> composable (otarget a) u v -> cone_compose (cone_compose a u) v = cone_compose a (comp (otarget a) u v). Proof. ir. assert (lem : cone_composable (cone_compose a u) v). uhg; ee. ap is_cone_cone_compose; try am. rw otarget_cone_compose. rwi composable_facts_rw H0; lu. rw vertex_cone_compose. sy; lu. assert (lem2 : cone_composable a (comp (otarget a) u v)). uhg; ee. lu. ap mor_comp. am. rw target_comp. lu. am. ap Nat_Trans.axioms_extensionality. ap cone_compose_axioms. am. ap cone_compose_axioms. am. rw nsource_cone_compose. rw nsource_cone_compose. rw osource_cone_compose. rw otarget_cone_compose. rw source_comp. tv. am. rw ntarget_cone_compose. rw ntarget_cone_compose. rw ntarget_cone_compose. tv. ir. rw ntrans_cone_compose. rw ntrans_cone_compose. rw ntrans_cone_compose. rw otarget_cone_compose. rw assoc. tv. ap show_composable. ap mor_ntrans. lu. am. tv. lu. rw cone_source_ntrans. sy; lu. lu. am. am. am. am. am. Qed. Lemma cone_compose_vcompose : forall a b u, cone_composable b u -> vcomposable a b -> cone_compose (vcompose a b) u = vcompose a (cone_compose b u). Proof. ir. assert (lem1: otarget a = otarget b). transitivity (ftarget (nsource a)). rww ftarget_nsource. lu. uf otarget. uh H0; ee. rww H2. uf cone_compose. rw vcompose_assoc. rw osource_vcompose. rw otarget_vcompose. rww lem1. am. uhg; ee. lu. ap constant_nt_axioms. rw osource_vcompose. lu. rw otarget_vcompose. lu. rw otarget_vcompose. rw lem1; lu. rw ntarget_constant_nt. uh H; ee. uh H; ee. uh H3; ee. rw H3. rw osource_vcompose. rw otarget_vcompose. rw fsource_nsource. rww ftarget_nsource. ufi vertex H2. wr H2. rw lem1. tv. Qed. Definition is_uni a := is_cone a & (forall u v, cone_composable a u -> cone_composable a v -> cone_compose a u = cone_compose a v -> u = v). Definition is_versal a := is_cone a & (forall b, is_cone b -> ntarget b = ntarget a -> (exists u, (cone_composable a u & cone_compose a u = b))). Definition is_limit a := is_uni a & is_versal a. Lemma is_limit_is_versal : forall a, is_limit a -> is_versal a. Proof. ir. lu. Qed. Lemma is_limit_is_uni : forall a, is_limit a -> is_uni a. Proof. ir. lu. Qed. Definition is_limit_of f a := is_limit a & ntarget a = f. Definition has_limit f := exists a, is_limit_of f a. Definition has_limits_over c b := (forall f, Functor.axioms f -> fsource f = c -> ftarget f = b -> has_limit f). Definition has_small_limits b := forall c, is_small c -> has_limits_over c b. Lemma nonempty_cat_data : nonemptyT (Category.data). Proof. ap nonemptyT_intro. ap Category.create; ir; exact False. Qed. Lemma nonempty_functor_data : nonemptyT (Functor.data). Proof. cp nonempty_cat_data. nin H. ap nonemptyT_intro. app Functor.create; ir; exact False. Qed. Lemma nonempty_nat_trans_data : nonemptyT (Nat_Trans.data). Proof. cp nonempty_functor_data. nin H. ap nonemptyT_intro. app Nat_Trans.create; ir; exact False. Qed. Definition limit f := chooseT (is_limit_of f) nonempty_nat_trans_data. Lemma if_has_limit : forall f, has_limit f -> is_limit_of f (limit f). Proof. ir. uh H. exact (chooseT_pr nonempty_nat_trans_data H). Qed. Lemma is_limit_limit : forall f, has_limit f -> is_limit (limit f). Proof. ir. cp (if_has_limit H). lu. Qed. Lemma ntarget_limit : forall f, has_limit f -> ntarget (limit f) = f. Proof. ir. cp (if_has_limit H). lu. Qed. Lemma nsource_limit : forall f, has_limit f -> nsource (limit f) = constant_functor (fsource f) (ftarget f) (vertex (limit f)). Proof. ir. cp (is_limit_limit H). uh H0; ee. uh H0; ee. uh H0; ee. uh H3. rw H3. rw fsource_nsource. rw ftarget_nsource. uf otarget. wr fsource_ntarget. rww ntarget_limit. am. am. Qed. Lemma vertex_vcompose : forall a u, vertex (vcompose u a) = vertex a. Proof. ir. tv. Qed. Lemma is_cone_vcompose : forall a u, is_cone a -> Nat_Trans.axioms u -> nsource u = ntarget a -> is_cone (vcompose u a). Proof. ir. uhg; ee. ap vcompose_axioms. am. lu. am. rw nsource_vcompose. lu. rw vertex_vcompose. rw otarget_vcompose. wr ftarget_nsource. rw H1. rw ftarget_ntarget. lu. am. Qed. Definition cone_create f v t := Nat_Trans.create (constant_functor (fsource f) (ftarget f) v) f t. Lemma nsource_cone_create : forall f v t, nsource (cone_create f v t) = constant_functor (fsource f) (ftarget f) v. Proof. ir. tv. Qed. Lemma ntarget_cone_create : forall f v t, ntarget (cone_create f v t) = f. Proof. ir. tv. Qed. Lemma ntrans_cone_create : forall f v t x, ob (fsource f) x -> ntrans (cone_create f v t) x = t x. Proof. ir. uf cone_create. rw ntrans_create_ob. tv. am. Qed. Lemma osource_cone_create : forall f v t, osource (cone_create f v t) = fsource f. Proof. ir. tv. Qed. Lemma otarget_cone_create : forall f v t, otarget (cone_create f v t) = ftarget f. Proof. ir. tv. Qed. Definition cone_property f v t := Functor.axioms f & ob (ftarget f) v & (forall x, ob (fsource f) x -> mor (ftarget f) (t x))& (forall x, ob (fsource f) x -> source (t x) = v)& (forall x, ob (fsource f) x -> target (t x) = fob f x)& (forall u, mor (fsource f) u -> comp (ftarget f) (fmor f u) (t (source u)) = t (target u)). Lemma cone_create_is : forall f v t, cone_property f v t -> is_cone (cone_create f v t). Proof. ir. uh H; ee. uhg; ee. uhg; ee. uf cone_create. ap create_like. lu. lu. rw nsource_cone_create. ap constant_functor_axioms. lu. lu. am. rw ntarget_cone_create. am. tv. rw ftarget_nsource. tv. uf cone_create. ap Nat_Trans.create_axioms. uhg; ee. ap constant_functor_axioms. lu. lu. am. am. rw fsource_constant_functor. tv. tv. ir. ap H1. am. ir. rw fob_constant_functor. ap H2; am. ir. ap H3; am. ir. rw fmor_constant_functor. rw right_id. sy. ap H4. am. rwi mor_facts_rw H5; lu. ap H1. rwi mor_facts_rw H5; lu. ap H2. rwi mor_facts_rw H5; lu. ir. rw otarget_cone_create. rw ntrans_cone_create. ap H1; am. am. ir. rw ntrans_cone_create. rw nsource_cone_create. rw fob_constant_functor. ap H2; am. am. ir. rw ntrans_cone_create. rw ntarget_cone_create. ap H3; am. am. ir. rw otarget_cone_create. rw ntrans_cone_create. rw nsource_cone_create. rw fmor_constant_functor. rw ntarget_cone_create. rw ntrans_cone_create. rw right_id. sy. ap H4. am. am. ap H1. rwi mor_facts_rw H5; lu. ap H2. rwi mor_facts_rw H5; lu. rwi mor_facts_rw H5; lu. rwi mor_facts_rw H5; lu. rw nsource_cone_create. ap constant_functor_is_constant. lu. am. am. Qed. Lemma ob_vertex : forall a, is_cone a -> ob (otarget a) (vertex a). Proof. ir. lu. Qed. Lemma is_cone_property : forall a, is_cone a -> cone_property (ntarget a) (vertex a) (ntrans a). Proof. ir. uh H; ee. uhg; ee. lu. am. ir. rw ftarget_ntarget. ap mor_ntrans. am. rwi fsource_ntarget H2. am. am. tv. ir. rw source_ntrans. uf vertex. uh H0. rw H0. uf constant_value. rw fob_constant_functor. rw fob_constant_functor. tv. am. rwi fsource_ntarget H2; am. ir. rwi fsource_ntarget H2. rw target_ntrans. tv. am. am. am. ir. rwi fsource_ntarget H2. rw ftarget_ntarget. cp H; uh H; ee. wr H13. uh H0. rw H0. rw fmor_constant_functor. rw ftarget_nsource. assert (constant_value (nsource a)= source (ntrans a (target u))). rw cone_source_ntrans. tv. uhg; ee; try am. rwi mor_facts_rw H2; lu. rw H14. rw right_id. tv. rw cone_source_ntrans. am. uhg; ee; am. rwi mor_facts_rw H2; lu. ap mor_ntrans. am. rwi mor_facts_rw H2; lu. tv. tv. am. am. am. Qed. Lemma comp_fmor_ntrans : forall a u, is_cone a -> mor (osource a) u -> comp (otarget a) (fmor (ntarget a) u) (ntrans a (source u)) = ntrans a (target u). Proof. ir. cp (is_cone_property H). uh H1; ee. ap H6. rw fsource_ntarget. am. uh H; ee; am. Qed. Definition cone_to_limit a b := choose (fun u => (cone_composable b u & cone_compose b u = a)). Lemma cone_to_limit_pr : forall a b, is_cone a -> is_versal b -> ntarget a = ntarget b -> (cone_composable b (cone_to_limit a b) & cone_compose b (cone_to_limit a b) = a). Proof. ir. uh H0; ee. util (H2 a). am. am. cp (choose_pr H3). cbv beta in H4. ee. am. util (H2 a). am. am. cp (choose_pr H3). cbv beta in H4. ee. am. Qed. Lemma mor_cone_to_limit : forall a b y, is_cone a -> is_versal b -> ntarget a = ntarget b -> y = otarget b -> mor y (cone_to_limit a b). Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. uh H3; ee. rw H2; am. Qed. Lemma source_cone_to_limit : forall a b, is_cone a -> is_versal b -> ntarget a = ntarget b -> source (cone_to_limit a b) = vertex a. Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. transitivity (vertex (cone_compose b (cone_to_limit a b))). rw vertex_cone_compose. tv. rw H3. tv. Qed. Lemma target_cone_to_limit : forall a b, is_cone a -> is_versal b -> ntarget a = ntarget b -> target (cone_to_limit a b) = vertex b. Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. uh H2; ee. am. Qed. Lemma cone_compose_cone_to_limit : forall a b, is_cone a -> is_versal b -> ntarget a = ntarget b -> cone_compose b (cone_to_limit a b) = a. Proof. ir. cp (cone_to_limit_pr H H0 H1). ee. am. Qed. Lemma cone_to_limit_cone_compose1 : forall a u, is_limit a -> cone_composable a u -> cone_to_limit (cone_compose a u) a = u. Proof. ir. uh H; ee. uh H; ee. ap H2. uhg; ee. am. ap mor_cone_to_limit. ap is_cone_cone_compose. am. am. rw ntarget_cone_compose. tv. tv. rw target_cone_to_limit. tv. ap is_cone_cone_compose. am. am. rw ntarget_cone_compose. tv. am. rw cone_compose_cone_to_limit. tv. ap is_cone_cone_compose. am. am. rw ntarget_cone_compose. tv. Qed. Lemma cone_to_limit_cone_compose : forall a b u, is_limit b -> cone_composable a u -> ntarget a = ntarget b -> cone_to_limit (cone_compose a u) b = comp (otarget b) (cone_to_limit a b) u. Proof. ir. set (k:= cone_to_limit a b). assert (lem1 : otarget b = otarget a). uf otarget. rw H1; tv. assert (lem2 : composable (otarget b) k u). ap show_composable. uf k. ap mor_cone_to_limit. lu. lu. am. tv. rw lem1. lu. uf k. rw source_cone_to_limit. sy; lu. lu. lu. am. assert (lem3: cone_compose b k = a). uf k. rw cone_compose_cone_to_limit. tv. lu. lu. am. wr lem3. rw cone_compose_cone_compose. rw cone_to_limit_cone_compose1. tv. am. uhg; ee. lu. ap mor_comp. am. rw target_comp. uf k. rw target_cone_to_limit. tv. lu. lu. am. am. uhg; ee. lu. rwi composable_facts_rw lem2; lu. uf k. rw target_cone_to_limit. tv. lu. lu. lu. am. Qed. Lemma cone_extensionality : forall a b, is_cone a -> is_cone b -> ntarget a = ntarget b -> vertex a = vertex b -> (forall x, ob (osource a) x -> ntrans a x = ntrans b x) -> a=b. Proof. ir. ap Nat_Trans.axioms_extensionality. lu. lu. uh H; ee. uh H0; ee. uh H4; ee. uh H6. rw H4. rw H6. assert (lem1: fsource (nsource a)= fsource (nsource b)). rw fsource_nsource. rw fsource_nsource. wr fsource_ntarget. wr fsource_ntarget. rw H1; tv. am. am. assert (lem2: ftarget (nsource a) = ftarget (nsource b)). rw ftarget_nsource. rw ftarget_nsource. uf otarget. rw H1; tv. am. am. assert (lem3 : constant_value (nsource a) = constant_value (nsource b)). am. rw lem1. rw lem2. rw lem3. tv. am. ir. au. Qed. Lemma cone_compose_id : forall a, is_cone a -> cone_compose a (id (otarget a) (vertex a)) = a. Proof. ir. ap cone_extensionality. ap is_cone_cone_compose. uhg; ee. am. ap mor_id. ap ob_vertex; am. rw target_id. tv. ap ob_vertex; am. am. rw ntarget_cone_compose. tv. rw vertex_cone_compose. rw source_id. tv. ap ob_vertex; am. ir. rw ntrans_cone_compose. rw right_id. tv. ap ob_vertex; am. ap mor_ntrans. lu. am. tv. rw cone_source_ntrans. tv. am. am. am. Qed. Lemma cone_to_limit_id : forall a b, is_limit a -> a = b -> cone_to_limit a b = id (otarget b) (vertex b). Proof. ir. cp H. uh H1; ee. uh H1; ee. ap H3. uhg; ee. am. ap mor_cone_to_limit. am. wr H0; lu. rw H0; tv. rw H0; tv. rw target_cone_to_limit. rw H0; tv. am. wr H0; lu. rw H0; tv. uhg; ee. am. wr H0; ap mor_id. ap ob_vertex. am. rw target_id. rw H0; tv. ap ob_vertex. wr H0; am. wr H0; rw cone_compose_cone_to_limit. rw cone_compose_id. tv. am. am. am. tv. Qed. Lemma comp_ntrans_cone_to_limit : forall r s x b, is_limit s -> is_cone r -> ntarget r = ntarget s -> b = otarget s -> ob (osource s) x -> comp b (ntrans s x) (cone_to_limit r s) = ntrans r x. Proof. ir. transitivity (ntrans (cone_compose s (cone_to_limit r s)) x). rw ntrans_cone_compose. rww H2. am. rw cone_compose_cone_to_limit. tv. am. ap is_limit_is_versal. am. am. Qed. Export Isomorphism. Lemma comp_cone_to_limit_inversely : forall a b c, is_limit a -> is_limit b -> ntarget a = ntarget b -> otarget a = c -> comp c (cone_to_limit a b) (cone_to_limit b a) = id c (vertex b). Proof. ir. assert (otarget b = c). uf otarget. wr H1. am. cp H; cp H0. uh H4; uh H5; ee. uh H4; uh H5. ee. assert (composable c (cone_to_limit a b) (cone_to_limit b a)). ap show_composable. app mor_cone_to_limit. sy; am. app mor_cone_to_limit. sy; am. sy; am. rww source_cone_to_limit. rww target_cone_to_limit. sy; am. ap H8. uhg; ee. am. rw H3. app mor_comp. rw target_comp. rww target_cone_to_limit. am. uhg; ee. am. rw H3. ap mor_id. wr H3. ap ob_vertex. am. rw target_id. tv. wr H3; app ob_vertex. wr H3. wr cone_compose_cone_compose. rww cone_compose_cone_to_limit. rw cone_compose_cone_to_limit. rw cone_compose_id. tv. am. am. am. sy; am. uhg; ee. am. app mor_cone_to_limit. rww target_cone_to_limit. rww H3. Qed. Lemma are_inverse_cone_to_limit : forall a b c, is_limit a -> is_limit b -> ntarget a = ntarget b -> otarget a = c -> are_inverse c (cone_to_limit a b) (cone_to_limit b a). Proof. ir. assert (otarget b = c). uf otarget. wr H1. am. cp H; cp H0. uh H4; uh H5; ee. uh H4; uh H5. ee. ap show_are_inverse. app mor_cone_to_limit. sy; am. app mor_cone_to_limit. sy; am. sy; am. rww source_cone_to_limit. rww target_cone_to_limit. sy; am. rww target_cone_to_limit. rww source_cone_to_limit. sy; am. rw source_cone_to_limit. app comp_cone_to_limit_inversely. am. am. sy; am. rww comp_cone_to_limit_inversely. rww source_cone_to_limit. sy; am. Qed. Lemma invertible_cone_to_limit : forall a b c, is_limit a -> is_limit b -> ntarget a = ntarget b -> otarget a = c -> invertible c (cone_to_limit a b). Proof. ir. uhg. sh (cone_to_limit b a). app are_inverse_cone_to_limit. Qed. Lemma inverse_cone_to_limit : forall a b c, is_limit a -> is_limit b -> ntarget a = ntarget b -> otarget a = c -> inverse c (cone_to_limit a b) = cone_to_limit b a. Proof. ir. cp (are_inverse_cone_to_limit H H0 H1 H2). app inverse_eq. Qed. Lemma is_limit_cone_compose : forall a u, is_limit a -> cone_composable a u -> invertible (otarget a) u -> is_limit (cone_compose a u). Proof. ir. assert (lem1: is_cone (cone_compose a u)). app is_cone_cone_compose. uhg; ee. (**** uni proof ****) uhg; ee. am. ir. assert (mor (otarget a) u0). lu. assert (mor (otarget a) v). lu. assert (source u = target u0). sy. lu. assert (source u = target v). sy. lu. assert (mor (otarget a) u). lu. rwi cone_compose_cone_compose H4. rwi cone_compose_cone_compose H4. uh H; ee. uh H; ee. assert (comp (otarget a) u u0 = comp (otarget a) u v). ap H11. uhg; ee. am. app mor_comp. app show_composable. rww target_comp. lu. app show_composable. uhg; ee. am. app mor_comp. app show_composable. rw target_comp. lu. app show_composable. lu. transitivity (comp (otarget a) (inverse (otarget a) u) (comp (otarget a) u u0)). wr assoc. rw left_inverse. rw left_id. tv. app ob_source. am. sy; am. am. app show_composable. ap mor_inverse. am. rw source_inverse. tv. am. app show_composable. rw H12. wr assoc. rw left_inverse. rw left_id. tv. app ob_source. am. sy; am. am. app show_composable. app mor_inverse. rww source_inverse. app show_composable. am. app show_composable. am. app show_composable. (*** versal proof ***) uhg; ee. am. ir. assert (lem2: composable (otarget a) (inverse (otarget a) u) (cone_to_limit b a)). ap show_composable. app mor_inverse. app mor_cone_to_limit. app is_limit_is_versal. rw source_inverse. rww target_cone_to_limit. lu. app is_limit_is_versal. am. sh (comp (otarget a) (inverse (otarget a) u) (cone_to_limit b a)). ee. uhg; ee. am. rw otarget_cone_compose. app mor_comp. rww target_comp. rww target_inverse. assert (otarget a = otarget (cone_compose a u)). rww otarget_cone_compose. rw H4. wr cone_compose_cone_compose. assert (cone_compose (cone_compose a u) (inverse (otarget (cone_compose a u)) u) = a). wr H4. rw cone_compose_cone_compose. rww right_inverse. assert (target u = vertex a). lu. rw H5. rww cone_compose_id. lu. am. app show_composable. lu. ap mor_inverse. am. rw target_inverse. tv. am. rw H5. rww cone_compose_cone_to_limit. app is_limit_is_versal. uhg; ee. app is_cone_cone_compose. rww otarget_cone_compose. app mor_inverse. rww otarget_cone_compose. rww target_inverse. am. Qed. Lemma cone_to_limit_invertible_is_limit : forall a b, is_limit b -> is_cone a -> ntarget a = ntarget b -> invertible (otarget b) (cone_to_limit a b) -> is_limit a. Proof. ir. assert (a = cone_compose b (cone_to_limit a b)). rw cone_compose_cone_to_limit. tv. am. app is_limit_is_versal. am. rw H3. ap is_limit_cone_compose. am. uhg; ee. lu. app mor_cone_to_limit. app is_limit_is_versal. rww target_cone_to_limit. lu. am. Qed. End Limit. Module Commutation. Export Fmor_Isomorphism. Export Limit. Section Commutation_Def. Variable f : Functor.data. Variables a b : Nat_Trans.data. Hypothesis cone_a : is_cone a. Hypothesis limit_b : is_limit b. Hypothesis fsource_otarget : fsource f = otarget a. Hypothesis f_functor : Functor.axioms f. Hypothesis compose_ntarg : fcompose f (ntarget a) = ntarget b. Lemma vertex_htrans_left : vertex (htrans_left f a) = fob f (vertex a). Proof. uf vertex. rw nsource_htrans_left. uf constant_value. rw fob_fcompose. tv. Qed. Lemma is_cone_htrans_left : is_cone (htrans_left f a). Proof. uhg; ee. ap htrans_left_axioms. am. cp cone_a; lu. am. rw nsource_htrans_left. ap is_constant_fcompose. uhg; ee. am. ap functor_axioms_nsource. cp cone_a; lu. rw ftarget_nsource. am. cp cone_a; lu. cp cone_a; lu. rw fsource_otarget; cp cone_a; lu. rw otarget_htrans_left. rw vertex_htrans_left. ap ob_fob. am. rw fsource_otarget. ap ob_vertex. am. Qed. Definition commutation := cone_to_limit (htrans_left f a) b. Lemma source_commutation : source commutation = fob f (vertex a). Proof. uf commutation. rw source_cone_to_limit. uf vertex. rw nsource_htrans_left. uf constant_value. rw fob_fcompose. tv. ap is_cone_htrans_left. app is_limit_is_versal. rw ntarget_htrans_left. am. Qed. Lemma target_commutation : target commutation = vertex b. Proof. ir. uf commutation. rw target_cone_to_limit. tv. ap is_cone_htrans_left. app is_limit_is_versal. rww ntarget_htrans_left. Qed. Lemma mor_commutation : mor (ftarget f) commutation. Proof. uf commutation. ap mor_cone_to_limit. ap is_cone_htrans_left. app is_limit_is_versal. rww ntarget_htrans_left. uf otarget. wr compose_ntarg. rw ftarget_fcompose. tv. Qed. Lemma cone_composable_commutation : cone_composable b commutation. Proof. uhg; ee. cp limit_b; lu. assert (otarget b = ftarget f). uf otarget. wr compose_ntarg. rw ftarget_fcompose. tv. rw H. ap mor_commutation. uf commutation. rw target_cone_to_limit. tv. ap is_cone_htrans_left. cp limit_b; lu. rw ntarget_htrans_left. lu. Qed. Lemma cone_compose_commutation : cone_compose b commutation = htrans_left f a. Proof. uf commutation. rw cone_compose_cone_to_limit. tv. ap is_cone_htrans_left. app is_limit_is_versal. rww ntarget_htrans_left. Qed. Lemma invertible_commutation_is_limit_htrans_left : forall c, ftarget f = c -> invertible c commutation = is_limit (htrans_left f a). Proof. ir. wr H. ap iff_eq; ir. wr cone_compose_commutation. app is_limit_cone_compose. ap cone_composable_commutation. assert (otarget b = ftarget f). uf otarget. wr compose_ntarg. rw ftarget_fcompose. tv. rww H1. uf commutation. ap invertible_cone_to_limit. am. am. rww ntarget_htrans_left. rw otarget_htrans_left. tv. Qed. End Commutation_Def. Section Htrans_Cone_Compose. Variable f:Functor.data. Variable a : Nat_Trans.data. Variable u : E. Hypothesis K : is_cone a. Hypothesis K0 : Functor.axioms f. Hypothesis K1 : fsource f = otarget a. Hypothesis K2 : mor (fsource f) u. Hypothesis K3 : target u = vertex a. Lemma cone_composable_a_u : cone_composable a u. Proof. uhg; ee. am. wr K1; am. am. Qed. Lemma htrans_left_cone_compose : htrans_left f (cone_compose a u) = cone_compose (htrans_left f a) (fmor f u). Proof. ap cone_extensionality. ap is_cone_htrans_left. ap is_cone_cone_compose. ap cone_composable_a_u. rww otarget_cone_compose. am. ap is_cone_cone_compose. uhg; ee. app is_cone_htrans_left. rww otarget_htrans_left. app mor_fmor. rww target_fmor. rww vertex_htrans_left. rww K3. rww ntarget_htrans_left. rww vertex_htrans_left. rww vertex_cone_compose. rww vertex_cone_compose. rww source_fmor. ir. rwi osource_htrans_left H. rwi osource_cone_compose H. rww ntrans_htrans_left. rww ntrans_cone_compose. wr K1; wrr comp_fmor. rww ntrans_cone_compose. rww otarget_htrans_left. rww ntrans_htrans_left. app show_composable. rw K1; app mor_ntrans. cp K; lu. rww source_ntrans. cp K. uh H0; ee. uh H1. rw H1. rww fob_constant_functor. sy; am. cp K; lu. Qed. End Htrans_Cone_Compose. Section Htrans_Cone_To_Limit. Variable f : Functor.data. Variables a b : Nat_Trans.data. Hypothesis K : Functor.axioms f. Hypothesis K0 : is_cone a. Hypothesis K1 : is_limit b. Hypothesis K2 : ntarget a = ntarget b. Hypothesis K3 : fsource f = otarget b. Hypothesis K4 : is_limit (htrans_left f b). Lemma cone_compose_htrans_left_fmor_cone_to_limit : cone_compose (htrans_left f b) (fmor f (cone_to_limit a b)) = htrans_left f a. Proof. assert (lem1 : a = cone_compose b (cone_to_limit a b)). rww cone_compose_cone_to_limit. cp K1; lu. transitivity (htrans_left f (cone_compose b (cone_to_limit a b))). rww htrans_left_cone_compose. cp K1; lu. rw K3. app mor_cone_to_limit. cp K1; lu. rww target_cone_to_limit. cp K1; lu. wr lem1. tv. Qed. Lemma fmor_cone_to_limit : fmor f (cone_to_limit a b) = cone_to_limit (htrans_left f a) (htrans_left f b). Proof. cp K4. uh H; ee. uh H; ee. assert (is_cone b). cp K1; lu. assert (is_versal b). cp K1; lu. ap H1. uhg; ee. app is_cone_htrans_left. rww otarget_htrans_left. app mor_fmor. rw K3. app mor_cone_to_limit. rww target_fmor. rww vertex_htrans_left. rww target_cone_to_limit. rw K3; app mor_cone_to_limit. uhg; ee. app is_cone_htrans_left. rww otarget_htrans_left. app mor_cone_to_limit. app is_cone_htrans_left. rw K3. uf otarget. rww K2. rww ntarget_htrans_left. rww ntarget_htrans_left. rww K2. rww target_cone_to_limit. app is_cone_htrans_left. rw K3; uf otarget; rww K2. rww ntarget_htrans_left. rww ntarget_htrans_left. rww K2. rww cone_compose_htrans_left_fmor_cone_to_limit. rww cone_compose_cone_to_limit. app is_cone_htrans_left. rw K3; uf otarget; rww K2. rw ntarget_htrans_left. rw ntarget_htrans_left. rww K2. Qed. End Htrans_Cone_To_Limit. Section Limit_Preservation_Invariance. Variable f : Functor.data. Variables a b : Nat_Trans.data. Hypothesis K : Functor.axioms f. Hypothesis K0 : is_limit a. Hypothesis K1 : is_limit b. Hypothesis K2 : ntarget a = ntarget b. Hypothesis K3 : fsource f = otarget b. Hypothesis K4 : is_limit (htrans_left f b). Lemma invertible_cone_to_limit_a_b: invertible (fsource f) (cone_to_limit a b). Proof. app invertible_cone_to_limit. rw K3; uf otarget; rw K2. tv. Qed. Lemma invertible_fmor_ctl : invertible (ftarget f) (fmor f (cone_to_limit a b)). Proof. app invertible_fmor. app invertible_cone_to_limit. rw K3; uf otarget; rww K2. Qed. Lemma limit_preservation_invariance : is_limit (htrans_left f a). Proof. ir. ap (cone_to_limit_invertible_is_limit (a:= (htrans_left f a)) (b:=(htrans_left f b))). am. app is_cone_htrans_left. cp K0; lu. rw K3; uf otarget; rww K2. rw ntarget_htrans_left. rw ntarget_htrans_left. rww K2. wr fmor_cone_to_limit. rw otarget_htrans_left. ap invertible_fmor_ctl. am. cp K0; lu. am. am. am. am. Qed. End Limit_Preservation_Invariance. End Commutation.