J. A. Carr 8 July 2025.

The untruncated form of the at-most-two elements is equivalent
to the statement that Aut Ξ© has exactly 1 or 2 elements
(and hence every element is either identity or negation)

\begin{code}

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

open import MLTT.Spartan
open import MLTT.Plus-Properties
open import UF.DiscreteAndSeparated
open import TypeTopology.SigmaDiscreteAndTotallySeparated
open import UF.Equiv hiding (_β‰…_)
open import UF.FunExt
open import UF.Logic
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.SubtypeClassifier hiding (Ξ©)
open import Fin.Type
open import Fin.Topology
open import Fin.Pigeonhole

module Higgs.UntruncatedAtMostTwo
        {𝓀 : Universe}
        (fe : Fun-Ext)
        (pe : propext 𝓀)
        (pt : propositional-truncations-exist)
       where

open import Higgs.Rigidity fe pe
open import Higgs.InvolutionTheorem fe pe
open import Higgs.AutomorphismsOfOmega fe pe
open import Higgs.AutomorphismsOfOmegaWEM fe pe pt

open Conjunction
open Implication fe
open Universal fe

\end{code}

Assuming function extensionality, having an untruncated pigeonhole principle
reflects discreteness to the codomain.

The core method is to note that the pidgeonhole function must respect equality
of functions, so we produce a pair of functions, where equality of their results
holds if and only if the two elements of the codomain are equal.

\begin{code}

constantly : {𝓀 π“₯ : Universe}
           β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
           β†’ Y β†’ X β†’ Y
constantly y _ = y

almost-constantly-inner : {𝓀 π“₯ : Universe}
                  β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ (x' : X) β†’ Y β†’ Y β†’ (x : X)
                  β†’ ((x' ＝ x) + (x' β‰  x))
                  β†’ Y
almost-constantly-inner _ y' y _ (inl _) = y'
almost-constantly-inner _ y' y _ (inr _) = y

almost-constantly : {𝓀 π“₯ : Universe}
                  β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                  β†’ is-discrete X
                  β†’ X β†’ Y β†’ Y β†’ X
                  β†’ Y
almost-constantly X-discrete x' y' y x =
 almost-constantly-inner x' y' y x (X-discrete x' x)

almost-constantly-eq : {𝓀 π“₯ : Universe}
                     β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     β†’ (X-discrete : is-discrete X)
                     β†’ (x : X)
                     β†’ (y' y : Y)
                     β†’ almost-constantly X-discrete x y' y x ＝ y'
almost-constantly-eq X-discrete x y' y =
 almost-constantly X-discrete x y' y x               ＝⟨refl⟩
 almost-constantly-inner x y' y x (X-discrete x x)   ＝⟨ I ⟩
 almost-constantly-inner x y' y x (inl refl)         ＝⟨refl⟩
 y'                                                  ∎
 where
  I : almost-constantly-inner x y' y x (X-discrete x x)
      ＝ almost-constantly-inner x y' y x (inl refl)
  I = ap (almost-constantly-inner x y' y x)
         (discrete-inl-refl X-discrete x)

almost-constantly-neq : {𝓀 π“₯ : Universe}
                      β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                      β†’ (X-discrete : is-discrete X)
                      β†’ (x' x : X)
                      β†’ (y' y : Y)
                      β†’ (x' β‰  x)
                      β†’ almost-constantly X-discrete x' y' y x ＝ y
almost-constantly-neq X-discrete x' x y' y Ξ½ =
 almost-constantly X-discrete x' y' y x               ＝⟨refl⟩
 almost-constantly-inner x' y' y x (X-discrete x' x)  ＝⟨ I ⟩
 almost-constantly-inner x' y' y x (inr ν)            ＝⟨refl⟩
 y                                                    ∎
 where
  I :  almost-constantly-inner x' y' y x (X-discrete x' x)
       ＝ almost-constantly-inner x' y' y x (inr ν)
  I = ap (almost-constantly-inner x' y' y x)
         (discrete-inr fe X-discrete x' x Ξ½)


almost-constantly-is-constant
 : {𝓀 π“₯ : Universe}
 β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
 β†’ (X-discrete : is-discrete X)
 β†’ (x' : X)
 β†’ (y y' : Y)
 β†’ y ＝ y'
 β†’ constantly y ＝ almost-constantly X-discrete x' y' y
almost-constantly-is-constant {_} {_} {X} {Y} X-discrete x' y _ refl = dfunext fe III
 where
  I : constantly y x' ＝ y
  I = refl

  II : (x : X)
     β†’ ((x' ＝ x) + (x' β‰  x))
     β†’ almost-constantly X-discrete x' y y x ＝ y
  II _ (inl refl) = almost-constantly-eq X-discrete x' y y
  II x (inr Ξ½) = almost-constantly-neq X-discrete x' x y y Ξ½

  III : (x : X) β†’ constantly y x' ＝ almost-constantly X-discrete x' y y x
  III x = I βˆ™ II x (X-discrete x' x) ⁻¹


at-most-discrete-gives-discrete
 : {𝓀 π“₯ : Universe}
 β†’ (X : 𝓀 Μ‡) (Y : π“₯ Μ‡)
 β†’ is-discrete X
 β†’ ((f : X β†’ Y) β†’ f has-a-repetition)
 β†’ is-discrete Y
at-most-discrete-gives-discrete X Y X-discrete f-ph y y' = V VI
 where

  repeat-indices : (X β†’ Y)
                 β†’ X Γ— X
  repeat-indices f =
    (Ξ» (x , x' , _) β†’ (x , x'))
    (f-ph f)

  repeat-is-repeat : (f : X β†’ Y)
                   β†’ let (x , x') = repeat-indices f
                     in f x ＝ f x'
  repeat-is-repeat f =
    let (x , x' , _ , pf) = f-ph f
    in pf

  repeat-distinct : (f : X β†’ Y)
                  β†’ let (x , x') = repeat-indices f
                    in x β‰  x'
  repeat-distinct f =
    let (x , x' , pf , _) = f-ph f
    in pf

  f₁ = constantly y
  ix₁ = repeat-indices f₁
  fβ‚‚ = almost-constantly X-discrete (pr₁ ix₁) y' y
  ixβ‚‚ = repeat-indices fβ‚‚

  I : y ＝ y' β†’ ix₁ ＝ ixβ‚‚
  I e = ap repeat-indices
           (almost-constantly-is-constant X-discrete (pr₁ ix₁) y y' e)

  II : (x : X)
     β†’ (pr₁ ix₁ β‰  x)
     β†’ y ＝ fβ‚‚ x
  II x ne = almost-constantly-neq X-discrete (pr₁ ix₁) x y' y ne ⁻¹

  III : fβ‚‚ (pr₁ ix₁) ＝ y'
  III = almost-constantly-eq X-discrete (pr₁ ix₁) y' y

  IV : ix₁ ＝ ixβ‚‚ β†’ y ＝ y'
  IV e =
   y                            ＝⟨ II (prβ‚‚ ix₁) (repeat-distinct f₁) ⟩
   fβ‚‚ (prβ‚‚ ix₁)                 ＝⟨ ap (fβ‚‚ ∘ prβ‚‚) e ⟩
   fβ‚‚ (prβ‚‚ ixβ‚‚)                 ＝⟨refl⟩
   fβ‚‚ (prβ‚‚ (repeat-indices fβ‚‚)) ＝⟨ repeat-is-repeat fβ‚‚ ⁻¹ ⟩
   fβ‚‚ (pr₁ (repeat-indices fβ‚‚)) ＝⟨refl⟩
   fβ‚‚ (pr₁ ixβ‚‚)                 ＝⟨ ap (fβ‚‚ ∘ pr₁) (e ⁻¹) ⟩
   fβ‚‚ (pr₁ ix₁)                 ＝⟨ III ⟩
   y'                           ∎

  V : is-decidable (ix₁ ＝ ixβ‚‚) β†’ is-decidable (y ＝ y')
  V (inl e) = inl (IV e)
  V (inr ne) = inr (ne ∘ I)

  VI : is-decidable (ix₁ ＝ ixβ‚‚)
  VI = Γ—-is-discrete X-discrete X-discrete ix₁ ixβ‚‚

\end{code}

We may write the untruncated form of the at-most-2 lemma in this form

\begin{code}

at-most-two-is-pigeonhole
 : {𝓀 : Universe}
 β†’ {X : 𝓀 Μ‡}
 β†’ ((x y z : X) β†’ (z ＝ x) + (x ＝ y) + (y ＝ z))
 β†’ (f : Fin 3 β†’ X)
 β†’ f has-a-repetition
at-most-two-is-pigeonhole at-most-2 f = II I
 where
  v1 v2 v3 : Fin 3
  v1 = inr ⋆
  v2 = inl (inr ⋆)
  v3 = inl (inl (inr ⋆))

  true-when-eq : Fin 3
               β†’ Fin 3
               β†’ 𝓀 ⁺ Μ‡
  true-when-eq (inl (inl _)) (inl (inl _)) = πŸ™
  true-when-eq (inl (inl _)) (inl (inr _)) = 𝟘
  true-when-eq (inl (inl _)) (inr _) = 𝟘

  true-when-eq (inl (inr _)) (inl (inl _)) = 𝟘
  true-when-eq (inl (inr _)) (inl (inr _)) = πŸ™
  true-when-eq (inl (inr _)) (inr _) = 𝟘

  true-when-eq (inr _) (inl (inl _)) = 𝟘
  true-when-eq (inr _) (inl (inr _)) = 𝟘
  true-when-eq (inr _) (inr _) = πŸ™

  v3-not-1 : v3 β‰  v1
  v3-not-1 e = 𝟘-elim (transport (true-when-eq v3) e ⋆)
  v1-not-2 : v1 β‰  v2
  v1-not-2 e = 𝟘-elim (transport (true-when-eq v1) e ⋆)
  v2-not-3 : v2 β‰  v3
  v2-not-3 e = 𝟘-elim (transport (true-when-eq v2) e ⋆)

  I : (f v3 ＝ f v1) + (f v1 ＝ f v2) + (f v2 ＝ f v3)
  I = at-most-2 (f v1) (f v2) (f v3)

  II : (f v3 ＝ f v1) + (f v1 ＝ f v2) + (f v2 ＝ f v3)
     β†’ f has-a-repetition
  II (inl e31)       = ( v3 , v1 , v3-not-1 , e31 )
  II (inr (inl e12)) = ( v1 , v2 , v1-not-2 , e12 )
  II (inr (inr e23)) = ( v2 , v3 , v2-not-3 , e23 )

aut-Ξ©-discrete-has-em
 : is-discrete (Aut Ξ©)
 β†’ (𝕗 : Aut Ξ©)
 β†’ (𝕗 ＝ π•šπ••) + (𝕗 β‰  π•šπ••)
aut-Ξ©-discrete-has-em aut-disc 𝕗 = aut-disc 𝕗 π•šπ••

untruncated-at-most-two-iff-em
 : ((f g h : Aut Ξ©) β†’ (h ＝ f) + (f ＝ g) + (g ＝ h))
 ↔ ((𝕗 : Aut Ξ©) β†’ (𝕗 ＝ π•šπ••) + (𝕗 β‰  π•šπ••))
untruncated-at-most-two-iff-em = (FW , BW)
 where
  FW : ((f g h : Aut Ξ©) β†’ (h ＝ f) + (f ＝ g) + (g ＝ h))
     β†’ ((𝕗 : Aut Ξ©) β†’ (𝕗 ＝ π•šπ••) + (𝕗 β‰  π•šπ••))
  FW at-most-two = aut-Ξ©-discrete-has-em
   (at-most-discrete-gives-discrete
    (Fin 3) (Aut Ξ©)
    Fin-is-discrete
    (at-most-two-is-pigeonhole at-most-two))

  I : {f g : Aut Ξ©}
    β†’ (f β‰  π•šπ••)
    β†’ (g β‰  π•šπ••)
    β†’ (f ＝ g)
  I {f} f-not g-not = ((not-id-is-not f-not em) βˆ™ (not-id-is-not g-not em) ⁻¹)
   where
    em = Ξ©-automorphism-distinct-from-π•šπ••-gives-EM (f , f-not)

  II : {f g h : Aut Ξ©}
     β†’ ((f ＝ π•šπ••) + (f β‰  π•šπ••))
     β†’ ((g ＝ π•šπ••) + (g β‰  π•šπ••))
     β†’ ((h ＝ π•šπ••) + (h β‰  π•šπ••))
     β†’ (h ＝ f) + (f ＝ g) + (g ＝ h)
  II (inl  ef) (inl  eg) (_      ) = inr (inl (ef βˆ™ eg ⁻¹))
  II (inl  _ ) (inr neg) (inr neh) = inr (inr (I neg neh))
  II (inl  ef) (inr neg) (inl  eh) = inl (eh βˆ™ ef ⁻¹)
  II (inr  _ ) (inl  eg) (inl  eh) = inr (inr (eg βˆ™ eh ⁻¹))
  II (inr nef) (inr neg) (_      ) = inr (inl (I nef neg))
  II (inr nef) (inl  _ ) (inr neh) = inl (I neh nef)

  BW : ((𝕗 : Aut Ξ©) β†’ (𝕗 ＝ π•šπ••) + (𝕗 β‰  π•šπ••))
     β†’ ((f g h : Aut Ξ©) β†’ (h ＝ f) + (f ＝ g) + (g ＝ h))
  BW em f g h = II (em f) (em g) (em h)


\end{code}