Martin Escardo, 15 August 2014.

Higgs' Involution Theorem. In any topos, if f : Ω → Ω is a
monomorphism, then it is an involution.

We adapt and prove the result in HoTT, using the propositional axiom
of univalence. (We don't rely on propositional resizing (or
impredicativity).)

There is a proof by diagram chasing with iterated pullbacks, in page
65 of Johnstone's Sketches of an Elephant, volume 1.

The proof given here is based on an exercise in page 160 of Lambek and
Scott's Introduction to Higher-Order Categorical Logic, attributed to
Scedrov. Thanks to Phil Scott for bringing my attention to this proof.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module HiggsInvolutionTheorem where

open import SpartanMLTT
open import Sets
open import SubtypeClassifier

left-cancellable : {i j : 𝕃} {X : 𝕌 i} {Y : 𝕌 j} → (f : X → Y) → 𝕌 (i ⊔ j)
left-cancellable f = ∀{x x'} → f x ≡ f x' → x ≡ x'

involutive : {i : 𝕃} {X : 𝕌 i} → (f : X → X) → 𝕌 i
involutive f = ∀{x} → f(f x) ≡ x

higgs : prop-univalence → (f : Ω → Ω)
→ left-cancellable f → involutive f
higgs hpu f cancelf {p} = cancelf(VII p)
where
ΩU : Ω-univalence
ΩU = Ω-from-prop-univalence hpu

I : (p : Ω) → f p ≡ ⊤ → p ≡ ⊤ → f ⊤ ≡ ⊤
I p r s = transport (λ p → f p ≡ ⊤) s r

II : (p : Ω) → f p ≡ ⊤ → f ⊤ ≡ ⊤ → p ≡ ⊤
II p r s = cancelf (trans r (sym s))

III : (p : Ω) → f p ≡ ⊤ → p ≡ f ⊤
III p r = ΩU (I p r) (II p r)

IV : (p : Ω) → f(f p) ≡ ⊤ → p ≡ ⊤
IV p r = cancelf(III (f p) r)

V : (p : Ω) → f(f(f p)) ≡ ⊤ → f p ≡ ⊤
V p r = IV (f p) r

VI : (p : Ω) → f p ≡ ⊤ → f(f(f p)) ≡ ⊤
VI p r = trans d r
where
a : f(f p) ≡ f ⊤
a = ap f r
b : f ⊤ ≡ p
b = sym (III p r)
c : f(f p) ≡ p
c = trans a b
d : f(f(f p)) ≡ f p
d = ap f c

VII : (p : Ω) → f(f(f p)) ≡ f p
VII p = ΩU (V p) (VI p)

\end{code}