example of a mathematical proof formalized by type theory rather than set theory. I've been reading on type theory, and it being a possible foundation of mathematics. I have to say it is all very abstract to me. I'm very used to using set theory to think about mathematical proofs, but I find it very hard to imagine using type theory to think about mathematical proofs (I hardly understand type theory yet btw). 
So in order to make it less abstract and more concrete: Can you give an example of a mathematical proof, and how it would be formalized in type theory, rather than in set theory?
For example, let's take the proposition:

Proposition. Let $x$ be a real number and $x_n$ a sequence of real numbers. Let $f$ be a function continuous at $x$). Then if $x_n$ converges to $x$, then $f(x_n)$ converges to $f(x)$.

The way I think about proving this formally, would be to state first the definition of $x_n$ converging to $x$:
$$\forall \epsilon_{\in\mathbb R},\exists N_{\in \mathbb N},\forall n_{\in \mathbb N}:\left[(e>0 \land n>N)\implies|x_n-x|<\epsilon\right]$$
Then we can do the same for continuity of $f$. And then we simply apply some basic deductive axioms to get to the conclusion. I won't write down all the steps because you can imagine what it looks like. 
I however, cannot imagine what the equivalent process would look like for type theory. Can you show how you would prove this theorem (or any other simpler theorem) formally using type theory rather than set theory and first order logic? 
 A: 
Can you give an example of a mathematical proof, and how it would be formalized in type theory, rather than in set theory?

Here is an example of a simple proof in Coq, which is based on dependent type theory.
Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m.
Proof.
  intros x n; elim n; simpl; auto with real.
  intros n0 H' m; rewrite H'; auto with real.
Qed.

And here is a longer proof of a different lemma:
Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n.
Proof.
  intros; elim n.
  simpl; cut (1 + 0 * x = 1).
  intro; rewrite H0; unfold Rle; right; reflexivity.
  ring.
  intros; unfold pow; fold pow;
    apply
      (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x))
        ((1 + x) * (1 + x) ^ n0)).
  cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)).
  intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1;
    rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1);
      apply Rplus_le_compat_l; elim n0; intros.
  simpl; rewrite Rmult_0_l; unfold Rle; right; auto.
  unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt;
    intro; fold (Rsqr x);
      apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1)));
        fold (x > 0) in H;
          apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))).
  rewrite (S_INR n0); ring.
  unfold Rle in H0; elim H0; intro.
  unfold Rle; left; apply Rmult_lt_compat_l.
  rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)).
  assumption.
  rewrite H1; unfold Rle; right; trivial.
Qed.

Coq allows you to define tactics (like the rewrite and intros tactics above), which help you do the proof. They have a bunch of built in ones as well.
