proposition: Lemma target_our_mval : forall y, ob a y-> target (our_mval y) = pointv y.
proof: Proof. ir. uf our_mval. rw target_cone_to_limit. tv. app is_cone_other_pt. app is_limit_pointl. rww socle_other_pt. rww socle_pointl. Qed.
imports: Arith colimits functor_cat