proposition: Lemma plv_axioms : Functor.axioms plv.
proof: Proof. uf plv. ap Functor.create_axioms. sh pointv. uhg; ee; try am; ir. app ob_pointv. rww restr_id. app mor_restr. rww source_restr. rww target_restr. rww restr_comp. app show_composable. Qed.
imports: Arith colimits functor_cat