proposition: Lemma fob_plv : forall x, ob a x -> fob plv x = pointv x.
proof: Proof. ir. uf fob. rww fmor_plv. rw source_plv. rww restr_id. rww source_id. app ob_pointv. rw source_plv. app mor_id. Qed.
imports: Arith colimits functor_cat