proposition: Lemma fhom_bounded : forall a b, Bounded.axioms (fhom a b).
proof: Proof. ir. cp (Bounded.trans_criterion (p:=fhom a b) (f:=fun g => Arrow.create a b g) (x:=Function_Set.function_set (morphisms a) (fun z =>morphisms b))). apply H. ir. sh (L (morphisms a) (fmor y)). ee. apply Function_Set.in_function_set_inc. apply Function_Set.in_fs_for_L. ir. change (is_mor b (fmor y y0)). ap mor_is_mor. uh H0; ee. wr H3. app mor_fmor. rw H2. ap is_mor_mor. wr H2. lu. am. uh H0; ee. uh H0; ee. uh H0; ee. ufi Umorphism.create H0. set (k:= fmor y). wr H0. uf k. wr H1. wr H2. ap uneq. ap Function.create_extensionality. tv. ir. tv. Qed.
imports: Arith nat_trans