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.|
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 Lifting Property
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:
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: