Related Subjects
Spaces As Types
The Formal Interval
HoTT uses an idea from topology, the interval.
represents the unit interval [0,1]
not totally ordered like classic interval.
is like a type but it is not a type. Instead a path is a primitive notion in HoTT.
used for variables i... with grammar r,s ::= 0  1  i  1r  r/\s  r\/s where:

Paths
Path_{A}x y behaves like a function out of the interval p: > A where:
Although is not a proper type so we can't have a function into it for example. 
Transport turns path into equivalence.
Presheaf
A 'presheaf' category is a special case of a functor category (see page here). It is a contravarient functor from a category 'C' to Set.
Since it is contravarient it is usually written:
C^{op}→Set
or
Set^{Cop}
There is more about presheaves on the page here.
Presheaf Example  Single Element SetA very simple example would be where C^{op} is a single element set (terminal object in set). Hom( C^{op}, Set) therefore contains set of single arrows, one for every element of the set. 

Presheaf Example  GraphHere C^{op} is a category with two objects E (for edge) and V (for vertex) also two arrows s (for source) and t (for target). This allows us to build a structure on top of set where the diagram on the right commutes. We can therefore build up complex graphs from individual vertices and edges. 

Presheaf  Interval


This diagram tries to relate this to cubical complex bases on combinatorial notation as described on page here.  
A slightly more complex complex: 
Combining intervals
Meet  
Join 
Modeling Algebra
Comparison with Intentional Type Theory
In ML intentional type theory a proposition is either proven or not, if it was not then it may, or may not, be true. Since proofs in HoTT are canonical then we have other possibilities, it may be true, false, neither or both, also it may be true in many ways. These values represent truth values of propositions which correspond to paths in a space. This situation with different truth values is related to the idea of topos in category theory.
ITT  HoTT 

Proposition a=b 
Path I>A 
Proof of that proposition Refl: a=a 
λi > x 
Free De Morgan Algebra
De Morgan algebra is a generalisation of boolean algebra without rule of excluded middle.
RecapSo if we have 2 points 'n' and 'n+0' are they on a path/surface? This corresponds to the proposition 'n=n+0'. If we we using Boolean logic this proposition would be either true or false. In ML type theory/constructive logic the proposition is either proven or its not, if its not then we can't say anything about it. Here the truth value is a free De Morgan algebra. 
Fibrations
A cubical complex might be thought of as a family of types where the cells are put into are hierarchy of types according to their dimension. These dimensions (and therefore types) are related by their boundary maps, 
Presheaves
Presheaves allow us to build a more complex object out of simpler objects.
If C is a category of primitive objects then the presheaf is:
F: C^{op }> Set
Objects of C  Morphism in C 

X 
f: X > Y 
where: F(X) is a set representing the ways X occurs inside F. 
where: 
see nlab site 
Cubical sets are presheaves
Sheaves are discussed on page here.
Kan Composition
More information about Kan composition on these sites:
 https://ncatlab.org/nlab/show/Kan+complex
 https://en.wikipedia.org/wiki/Kan_fibration
 http://www.cse.chalmers.se/~coquand/stockholm.pdf
More information about Kan extensions on page here.