proposition: Lemma graph_morphism_is_F_bisimulation (S1 S2:F_coalgebra) (f:S1.(states)->S2.(states)) : (forall s1, lift_F_ _ _ f (S1.(transition) s1) = S2.(transition) (f s1)) -> is_F_bisimulation S1 S2 (fun x y=>y=f x).
proof: Proof. intros hypf. set (G_f:=fun x y=>y=f x). set (R_:={s1s2 : states S1 * states S2 | G_f (fst s1s2) (snd s1s2)}). set (fst_inv:=(fun s1:S1.(states)=> exist (fun s1s2=>snd s1s2=f (fst s1s2)) (s1,f(s1)) (refl_equal (f s1))) : S1.(states) -> R_). exists (fun r_:R_ => lift_F_ _ _ fst_inv (S1.(transition) (fst (proj1_sig r_)))). fold R_. intros [[s1 s2] hyp]; simpl; do 2 rewrite lift_F_compose; split. symmetry; apply lift_F_id. rewrite hyp; simpl; rewrite <- (hypf s1); apply lift_F_extensionality; trivial. Qed.
imports: ExtensionalFunctor Setoid