ホモトピー

反射律：$H(x,t):=f(x)$ は $X\times[0,1]\to X\to Y$（射影と $f$ の合成）なので連続であり、$H_0=H_1=f$、$A$ 上では $t$ によらず $f(a)$ をとる。
対称律：$H\colon f\simeq g\ \mathrm{rel}\ A$ に対し $H'(x,t):=H(x,1-t)$ とおく。$(x,t)\mapsto(x,1-t)$ は $X\times[0,1]$ の同相写像なので $H'$ は連続であり、$H'_0=H_1=g$、$H'_1=H_0=f$、$a\in A$ では $H'(a,t)=H(a,1-t)=f(a)$ である。
推移律：$H\colon f\simeq g\ \mathrm{rel}\ A$、$G\colon g\simeq h\ \mathrm{rel}\ A$ に対し
$$ K(x,t):=\begin{cases}H(x,2t)&(0\le t\le1/2)\\ G(x,2t-1)&(1/2\le t\le1)\end{cases} $$
とおく。$X\times[0,1/2]$ と $X\times[1/2,1]$ は $X\times[0,1]$ の閉集合で、その和は全体であり、共通部分 $X\times\{1/2\}$ の上で二つの式は $H(x,1)=g(x)=G(x,0)$ と一致する。よって貼り合わせの補題（Mun00 §18 Theorem 18.3）により $K$ は連続である。$K_0=H_0=f$、$K_1=G_1=h$ であり、$a\in A$ では両方の式が $f(a)$ をとる。$\square$

$H\colon f_1\simeq f_2$ とすると、$g_1\circ H\colon X\times[0,1]\to Z$ は連続写像の合成として連続で、$(g_1\circ H)_0=g_1\circ f_1$、$(g_1\circ H)_1=g_1\circ f_2$ である。$H$ が $A$ を固定すれば $g_1\circ H$ も $A$ を固定する。次に $G\colon g_1\simeq g_2$ とすると、$G\circ(f_1\times\operatorname{id}_{[0,1]})\colon(x,t)\mapsto G(f_1(x),t)$ は連続で、$t=0,1$ でそれぞれ $g_1\circ f_1$、$g_2\circ f_1$ をとる。$G$ が $B$ を固定すれば、$f_1(x)\in B$ となる $x$、すなわち $x\in f_1^{-1}(B)$ でこのホモトピーは $t$ によらない。最後に $g_1\circ f_1\simeq g_1\circ f_2\simeq g_2\circ f_2$ を homotopy-prop-equivalence-relation の推移律でつなぐ。$\square$

1. $f$ が同相写像なら $g:=f^{-1}$ について $g\circ f=\operatorname{id}_X$、$f\circ g=\operatorname{id}_Y$ が等号で成り立ち、homotopy-prop-equivalence-relation の反射律によりホモトピックでもある。
2. $f\colon X\to Y$、$f'\colon Y\to Z$ をホモトピー同値写像、$g$、$g'$ をそれぞれのホモトピー逆写像とする。homotopy-prop-composition を繰り返し使うと
   $$ (g\circ g')\circ(f'\circ f)=g\circ(g'\circ f')\circ f\simeq g\circ\operatorname{id}_Y\circ f=g\circ f\simeq\operatorname{id}_X $$
   であり、同様に $(f'\circ f)\circ(g\circ g')\simeq\operatorname{id}_Z$ である。よって $g\circ g'$ が $f'\circ f$ のホモトピー逆写像である。
3. 反射性は (1) を $\operatorname{id}_X$ に適用すればよい。対称性は定義が $f$ と $g$ について対称であることによる。推移性は (2) による。
4. $g$ を $f$ のホモトピー逆写像とすると、homotopy-prop-composition により $g\circ f'\simeq g\circ f\simeq\operatorname{id}_X$、$f'\circ g\simeq f\circ g\simeq\operatorname{id}_Y$ である。$\square$

1. 合成が代表元の取り方によらないことは homotopy-prop-composition そのものである。結合律 $([h]\circ[g])\circ[f]=[h\circ g\circ f]=[h]\circ([g]\circ[f])$ と、恒等射 $[\operatorname{id}_X]$ が単位であることは、写像の合成の結合律と恒等写像の性質から代表元の段階で成り立つ。$f\mapsto[f]$ が合成と恒等射を保つことは合成の定義そのものである。
2. $g$ が $f$ のホモトピー逆写像であることは $[g]\circ[f]=[\operatorname{id}_X]$、$[f]\circ[g]=[\operatorname{id}_Y]$ と同値であり、これは $[g]$ が $[f]$ の逆射であることにほかならない。
3. $F(f)$ が $[f]$ にしかよらないので、$[f]\mapsto F(f)$ は $\mathrm{hTop}$ 上で矛盾なく定義され、$F$ が関手であることから合成と恒等射を保つ。$g$ を $f$ のホモトピー逆写像とすると $F(g)\circ F(f)=F(g\circ f)=F(\operatorname{id}_X)=\operatorname{id}_{F(X)}$、同様に $F(f)\circ F(g)=\operatorname{id}_{F(Y)}$ なので $F(f)$ は同型射である。$\square$

$H_i\colon f_i\simeq g_i$ に対し $H(x_1,x_2,t):=(H_1(x_1,t),H_2(x_2,t))$ とおく。各成分は連続写像と射影の合成なので連続であり、直積位相の普遍性により $H$ は連続で、$H_0=f_1\times f_2$、$H_1=g_1\times g_2$ である。
後半：写像が矛盾なく定義されることは homotopy-prop-composition による。全射性：$[h_1]\in[X,Y_1]$、$[h_2]\in[X,Y_2]$ に対し $h:=(h_1,h_2)\colon X\to Y_1\times Y_2$ は直積位相の普遍性により連続で、$p_i\circ h=h_i$ である。単射性：$p_1\circ h\simeq p_1\circ h'$ と $p_2\circ h\simeq p_2\circ h'$ を与えるホモトピーを $K_1,K_2$ とし、$K(x,t):=(K_1(x,t),K_2(x,t))$ とおくと、$K$ は連続で $K_0=(p_1\circ h,p_2\circ h)=h$、$K_1=h'$ である。$\square$

$H\colon c_{y_0}\simeq c_{y_1}$ とすると、$x\in X$ を一つ固定して $\gamma(t):=H(x,t)$ とおけば $\gamma$ は $y_0$ から $y_1$ への道である。逆に道 $\gamma$ があれば $H(x,t):=\gamma(t)$ が求めるホモトピーである。後半：$X$ が可縮なら任意の $h\colon X\to Y$ はある定値写像 $c_{y}$ とホモトピックであり（homotopy-ex-contractible）、$[c_y]$ は $y$ の成分だけで決まる。よって $[h]\mapsto$（$y$ の属する成分）は矛盾なく定義された全射であり、前半により単射である。$\square$