First the type theory part of homotopy type theory. Mathematicians have been doing logic for a long time, but mathematical statements and proofs were not themselves mathematical objects. They were just human language text with some math notation thrown in. Around 1900 Brouwer, Heyting and Komolgorov came up with a cool idea: treat proofs as first class mathematical objects. Then giving a proof is equivalent to constructing a mathematical object.

* A proof of `P and Q` is a pair of proofs (a,b) where a is a proof of P and b is a proof of Q

* A proof of `P implies Q` is a function that takes a proof of P and returns a proof of Q

* A proof of `P or Q` is a pair (x,c) where either x=0 and c is a proof of P or x=1 and c is a proof of Q

In modern terms; to give a proof of `P and Q` is to give a value of the pair type `(P, Q)`. To give a proof of `P or Q` is to give a value of the disjoint sum type `P + Q`. To give a proof of `P implies Q` is to give a value of the function type `P -> Q`.

Take the theorem `(A and B) implies (B and A)`. A proof of this is, in Haskell notation:

proof :: (A,B) -> (B,A)
proof (a,b) = (b,a)

So a proof of `(A and B) implies (B and A)` is a function that swaps the order of a pair.

An interesting property of this way of doing things is that statements are not merely true or false, but statements can in general be true in more than one way. For example the statement `(A and A) implies A` has two different proofs:

proof1 :: (A,A) -> A
proof1 (a1,a2) = a1

proof2 :: (A,A) -> A
proof2 (a1,a2) = a2

The proof1 of `(A and A) implies A` is a function that returns the first component of a pair, and proof2 a function that returns the second component.

I'll skip over dependent types.

That's the type theory part. Now the homotopy part. For a long time there was a problem with type theory. There was no really good way to do equality in it. To do math you want to use equality all the time. Since we've defined what the proofs of `P and Q`, `P or Q`, `P implies Q` are, what are the proofs of `x = y`? There has existed some notion of equality in type theory for a long time, but it wasn't satisfactory for various reasons. You couldn't prove two functions equal even though they gave the same outputs for the same inputs. Homotopy type theory fixes equality in type theory. The idea is that a proof of `x = y` depends on the type of x and y.

* Two pairs c,d are equal if their first components are equal and their second components are equal.

* Two functions f,g are equal if for all x, f x is equal to g x.

* etc.

More precisely, the proofs of equality on the type (A,B) is a pair of a proof of equality on A and a proof of equality on B. Just like previously a statement can be true in more than one way (have more than one proof), things can now also be equal in more than one way (have more than one proof of equality).

Another extension that homotopy theory theory does is with user defined types. When you define a type you are allowed to define its type of equality proofs at the same time. This allows you to define things like integers modulo k ((i mod k) is equal to (i+k mod k)), unordered sets (a set S is equal to any permutation of S), and more.

I've brushed over a lot of details and presented only a very narrow way of looking at type theory:

1. A type itself is a value.

2. Full dependent types.

3. When are two types equal?

4. When are two proofs of equality equal?

5. What exactly is a function, what is a pair, etc.? This leads us into category theory, which gives an abstract description of functions and pairs.

Hopefully this still made some amount of sense.

Two line summary:

1. Type theory: using conventional mathematical objects like pairs and functions as proof objects.

2. Homotopy type theory: extends type theory with proofs of equality in a proper way.