proposition: Lemma IsFull_comp : Full_law F1 -> Full_law G1 -> let H1 := fun (a b : C) (h : G (F a) --> G (F b)) => F1 (G1 h) in Full_law (F:=F o_F G) H1.
proof: Proof. intros p1 p2. unfold Full_law in |- *; intros a b h. unfold FMor in |- *; simpl in |- *; unfold Comp_FMor, Comp_FOb in |- *. apply Trans with (FMor G (G1 h)). apply (p2 _ _ h). apply FPres. apply (p1 _ _ (G1 h)). Qed.
imports: Functor CatProperty