Non-Euclidean geometry: spherical and hyperbolic

A pilot flies from the North Pole due south to the equator, turns to fly a quarter of the way around the equator, and then flies due north back to the pole. What is the angle sum of this triangle, in degrees?

A triangle on a sphere of radius $2$ has angles $\frac{\pi}{2}$, $\frac{\pi}{2}$ and $\frac{\pi}{3}$. Its area is $\frac{k\pi}{3}$. What is $k$?

A triangle in the hyperbolic plane (curvature $-1$) has three angles of $\frac{\pi}{6}$ each. What is its area?

Which of these curves are lines (geodesics) of the upper half-plane model $\mathbb H$? (Choose all that apply.)

What is the hyperbolic distance in $\mathbb H$ between $i$ and $e^3 i$?

In the theorem that $g(z) = \frac{az + b}{cz + d}$ is an isometry of $\mathbb H$ we required $a, b, c, d$ real with $ad - bc = 1$. What goes wrong for $g(z) = -z$, which has $a = -1$, $b = c = 0$, $d = 1$ and $ad - bc = -1$?

The Lean theorem many_parallels states: for c : ℝ with 1 ≤ c and y : ℝ with 0 < y, normSq (I * y - c) ≠ normSq (1 + I - c). What does it say geometrically?

Why does the upper half-plane model show that the parallel postulate cannot be proved from the other axioms of plane geometry?

Write hyp_dist(z, w) for points of the upper half-plane (Python complex numbers with positive imaginary part), using $\cosh d = 1 + \frac{|z - w|^2}{2\operatorname{Im} z \operatorname{Im} w}$, and defect(z1, z2, z3), the defect $\pi - (\alpha + \beta + \gamma)$ of the triangle, computing each angle from the side lengths by the hyperbolic law of cosines $\cos\gamma = \frac{\cosh a \cosh b - \cosh c}{\sinh a \sinh b}$ (where $c$ is the side opposite $\gamma$).