proposition: Lemma dotted_unique : forall f u, Functor.axioms f -> has_limit f -> cone_composable (limit f) u -> dotted (cone_compose (limit f) u) = u.
proof: Proof. ir. rw dotted_cone_compose. rw dotted_limit. rw cone_target_limit. rw left_id. tv. assert (target f = cone_target (limit f)). rww cone_target_limit. rw H2. app ob_vertex. ap is_limit_is_cone. app is_limit_limit. uh H1; ee. rwi cone_target_limit H2. am. am. uh H1; ee. am. tv. am. am. am. am. rww socle_limit. Qed.
imports: Arith nat_trans