proposition: Lemma laws_of_faithful_functor {h l X Y} {L: laws h Y} {Hl: l ≪ h} f' f: @functor l X Y f' f -> (forall n m x y, f n m x ≦ f n m y -> x ≦ y) -> (forall n m x y, f n m x ≡ f n m y -> x ≡ y) -> laws l X.
proof: Proof. intros Hf Hleq Hweq. assert (Hleq_iff: forall n m x y, f n m x ≦ f n m y <-> x ≦ y). split. apply Hleq. apply fn_leq. assert (Hweq_iff: forall n m x y, f n m x ≡ f n m y <-> x ≡ y). split. apply Hweq. apply fn_weq. assert (L' := @lower_laws _ _ _ L Hl). constructor; repeat right; intro_vars. apply (laws_of_injective_morphism (f n m)); auto using fn_morphism. rewrite <-Hweq_iff, 4fn_dot. apply dotA. rewrite <-Hweq_iff, fn_dot, fn_one. apply dot1x. rewrite <-Hweq_iff, fn_dot, fn_one. apply dotx1. repeat intro. apply Hleq. rewrite 2fn_dot. now apply dot_leq; apply Hleq_iff. apply Hleq. now rewrite fn_cup, 3fn_dot, fn_cup, dotplsx. apply Hleq. now rewrite fn_cup, 3fn_dot, fn_cup, dotxpls. apply Hleq. now rewrite fn_dot, 2fn_bot, dot0x. apply Hleq. now rewrite fn_dot, 2fn_bot, dotx0. intro. apply Hleq. now rewrite fn_cnv, 2fn_dot, 2fn_cnv, cnvdot. intro. rewrite <-Hweq_iff, 2fn_cnv. apply cnv_invol. repeat intro. apply Hleq. rewrite 2fn_cnv. now apply cnv_leq; apply Hleq_iff. apply Hleq. rewrite 2fn_dot,fn_cnv. apply cnv_ext. intro. apply Hleq. rewrite fn_one, fn_str. apply str_refl. intro. apply Hleq. rewrite fn_str, fn_dot, fn_str. apply str_cons. intro. rewrite <-2Hleq_iff, 2fn_dot, fn_str. apply str_ind_l. rewrite <-2Hleq_iff, 2fn_dot, fn_str. apply str_ind_r. intro. apply Hweq. rewrite fn_itr, fn_dot, fn_str. apply itr_str_l. intro. apply Hleq. rewrite fn_cap,2fn_dot,fn_cap,fn_dot,fn_cnv. apply capdotx. intro. rewrite <-2Hleq_iff, fn_dot, fn_ldv. apply ldv_spec. intro. rewrite <-2Hleq_iff, fn_dot, fn_rdv. apply rdv_spec. Qed.
imports: lattice