Definition 1
Here is one definition of continuity, based on open sets:
Let X and Y be topological spaces. A function f : X>Y is continuous if f^{1}(V) is open for every open set V in Y. 
Definition 2
Another definition of continuity, based on neighbourhoods, is equivilant to the above definition.
Let X and Y be topological spaces. A function f : X>Y is continuous if for every xX and every open set U containing f(x), there exists a neighbourhood V of x such that f(V)U. 
Homotopy
Fibrations
Homotopy Lifting Property
https://en.wikipedia.org/wiki/Homotopy_lifting_property
Transport
from here  transport : Path U A B > A > B 
That is, if we have a path from A to B and A, then B.
Composition of Paths
We want to compose these two paths:

from here 
compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c = comp (<_> A) (p @ i) [ (i = 0) > Where 'comp' is a keyword with the following parameters:
