proposition: Lemma dotted_limit : forall f, Functor.axioms f -> has_limit f -> dotted (limit f) = id (target f) (vertex (limit f)).
proof: Proof. ir. uf dotted. rww socle_limit. rw cone_to_limit_refl. rw cone_target_limit. tv. am. app is_limit_limit. Qed.
imports: Arith nat_trans