In order to understand what exactly is meant by path in homotopy type theory, I am looking into homotopies. This led to the following questions (some definitions follow):
- Intuition for how "continuous" works in a discrete system. If a continuous function in a discrete graph/topology is really just moving along an edge at each step. Homotopy relies on the definition of continuity, so I'm wondering what it means in the discrete case. Just want to make sure I'm understanding the wikipedia quote (below).
- How to show/prove two functions (on a discrete topology) are homotopic. Say I have two functions $x$ and $y$. They take 1 parameter.
Computationally (not sure if this matters) $x$ takes 3 computations to return its output, and $y$ takes 5.They both create different output that is isomorphic to each other. $x(a) = p$ and $y(a) = q$, where $p$ and $q$ are isomorphic. How to show/prove they are homotopic (if at all). If they're not homotopic, what is an example of homotopy (in a discrete topology), and how to show they are homotopic.
These definitions are from Wikipedia, I can mostly follow them.
A continuous function is:
- A function $f : X \to Y$ (between two topological spaces $X$ and $Y$)
- For every open set $V \subseteq Y$, the inverse image is an open subset of X. $$f^{-1}(V)=\{x\in X\;|\;f(x)\in V\}$$
An extreme example: if a set $X$ is given the discrete topology (in which every subset is open), all functions $f\colon X\rightarrow T$ to any topological space $T$ are continuous.
A homotopy is:
- Defined as two continuous functions $f$ and $g$
- From topological space $X$ to $Y$
- That can be continuously deformed into one another
- Formally, $H : X \times [0,1] \to Y$
- Such that: $x \in X \Rightarrow H(x,0) = f(x) \land H(x,1) = g(x)$
We can also think of the second parameter as a "slider control" that allows us to smoothly transition from f to g as the slider moves from 0 to 1, and vice versa.