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.

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.

We use type-in-type because our libraries are not universe polymorphic
at the moment.


{-# OPTIONS --without-K #-}
{-# OPTIONS --type-in-type #-}

module HiggsInvolutionTheorem where

open import HSets
open import SetsAndFunctions
open import Equality
open import SubtypeClassifier

left-cancellable : {X Y : U}  (f : X  Y)  U
left-cancellable f = ∀{x x'}  f x  f x'  x  x'

involutive : {X : U}  (f : X  X)  U
involutive f = ∀{x}  f(f x)  x

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

   I : (p : Ω)  f p    p    f    
   I p r s = subst {Ω}  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
     a : f(f p)  f 
     a = cong 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 = cong f c

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