/-- **Every natural family of maps `X × X → X` is a projection.** Suppose `α X : X × X → X` is
given for every type `X`, and is natural: `α Y (f a, f b) = f (α X (a, b))` for every function
`f : X → Y`. Then either `α X (a, b) = a` for all `X, a, b`, or `α X (a, b) = b` for all.
Proof (as in the lesson). Look at one test case: the pair `(true, false)` in the two-element type
`B`. For any `X` and `(a, b)`, the function `f : B → X` with `f true = a`, `f false = b` sends
`(true, false)` to `(a, b)`, so naturality gives `α X (a, b) = f (α B (true, false))`. Hence the
whole family is decided by one value, `α B (true, false)`, which is `true` (projection to `a`) or
`false` (projection to `b`). `ULift` moves `Bool` into the universe `u`. -/
theorem natural_sq_to_id (α : ∀ X : Type u, X × X → X)
(nat : ∀ (X Y : Type u) (f : X → Y) (p : X × X), α Y (f p.1, f p.2) = f (α X p)) :
(∀ (X : Type u) (p : X × X), α X p = p.1) ∨ (∀ (X : Type u) (p : X × X), α X p = p.2) := by
-- Every component is determined by the single value `α B (true, false)`.
have key : ∀ (X : Type u) (p : X × X),
α X p = (if (α (ULift.{u} Bool) (⟨true⟩, ⟨false⟩)).down then p.1 else p.2) := by
intro X p
have h := nat (ULift.{u} Bool) X (fun b => if b.down then p.1 else p.2) (⟨true⟩, ⟨false⟩)
simpa using h
rcases h : α (ULift.{u} Bool) (⟨true⟩, ⟨false⟩) with ⟨b⟩
cases b
· right
intro X p
rw [key, h]
rfl
· left
intro X p
rw [key, h]
rfl