Here's a rough summary. Homotopy type theory is about proofs of equality. Proofs of equality can have computational content. For example, a proof that two types A,B are equal is given by an isomorphism f : A -> B, f^-1 : B -> A, such that f . f^-1 = id (in homotopy type theory that is further generalized to the concept of equivalence). A proof that two functions f,g : A -> B are equal is given by a function that takes an x:A and returns a proof that f x = g x for every such x. In particular in homotopy type theory it is not the case that if two things are proven equal, then they are identical. For example the type of integers is equal to the type of naturals (positive integers), because you can give an isomorphism, but it's not identical because they are two different types. On the other hand the type of booleans is neither identical nor equal to the type of integers, because there isn't an isomorphism. Homotopy type theory allows user defined types where you can have equality between two values that aren't identical. These are called higher inductive types. An example of this is the type of finite sets represented as lists. The list [1,2,3] and [2,3,1] represent the same set, but they aren't identical. They do however represent equal sets. One of the key points of homotopy type theory is that if you want to give a function f : A -> B where the type A has values that are equal but not identical, then you have to give a proof that whenever x1:A is equal to x2:A, then f x1 is equal to f x2. In other words, functions have to respect equalities. For example we can define a function on finite sets by given a function on finite lists, but in order to make that a function on finite sets we have to give a proof that the output of that function does not depend on the order of the input list. Similar ideas crop up all over the place. The most well known is perhaps the idea that a mathematical description of physics should not depend on the coordinate system you choose.