Automorphisms of 𝟙 + LEM in agda-unimath

AutLEM.agda

-- What exactly are the correct flags to use?
{-# OPTIONS --without-K -WnoWithoutKFlagPrimEraseEquality --guardedness #-}
open import foundation

postulate
  l : Level

X : UU (lsuc l)
X = unit + LEM l

LEM-ext : (lem lem' : LEM l) → lem ＝ lem'
LEM-ext lem lem' = center (is-prop-type-Prop (prop-LEM l) lem lem')

swap : LEM l → Aut X
swap lem = equiv-involution (pair action involutive) where

   action : X → X
   action (inl star) = inr lem
   action (inr lem') = inl star

   involutive : is-involution action
   involutive (inl star) = refl
   involutive (inr lem') = ap inr (LEM-ext lem lem')

inl-action-id : (F : Aut X) → (map-equiv F (inl star) ＝ inl star) → F ＝ id-equiv
inl-action-id F F-inl-eq = eq-htpy-equiv pointwise where

  pointwise : (x : X) → map-equiv F x ＝ x
  pointwise (inl star) = F-inl-eq
  pointwise (inr lem) with map-equiv F (inr lem) in F-inr-eq
  ... | inr lem' = ap inr (LEM-ext lem' lem)
  ... | inl star = is-injective-equiv F (F-inl-eq ∙ inv F-inr-eq)

inl-action-swap : (F : Aut X) → (lem : LEM l) → map-equiv F (inl star) ＝ inr lem → F ＝ swap lem
inl-action-swap F lem F-inl-eq = eq-htpy-equiv pointwise where

  pointwise : (x : X) → map-equiv F x ＝ map-equiv (swap lem) x
  pointwise (inl star) = F-inl-eq
  pointwise (inr lem') rewrite LEM-ext lem' lem with map-equiv F (inr lem) in F-inr-eq
  ... | inl star = refl
  ... | inr lem'' rewrite LEM-ext lem'' lem = is-injective-equiv F (F-inr-eq ∙ inv F-inl-eq)

-- Did I miss this somewhere in agda-unimath?
coproduct-is-set : {l1 l2 : Level} (A : UU l1) (B : UU l2) → is-set A → is-set B → is-set (A + B)
coproduct-is-set A B A-set B-set s t rewrite eq-equiv (extensionality-coproduct s t) = is-prop-all-elements-equal case where

  case : all-elements-equal (Eq-coproduct s t)
  case (Eq-eq-coproduct-inl p1) (Eq-eq-coproduct-inl p2) = ap Eq-eq-coproduct-inl (center (A-set _ _ p1 p2))
  case (Eq-eq-coproduct-inr p1) (Eq-eq-coproduct-inr p2) = ap Eq-eq-coproduct-inr (center (B-set _ _ p1 p2))

requirement0 : is-set (Aut X)
requirement0 = is-set-Aut X-set where

  is-set-LEM : is-set (LEM l)
  is-set-LEM = is-set-is-prop (is-prop-type-Prop (prop-LEM l))

  X-set : is-set X
  X-set = coproduct-is-set unit (LEM l) is-set-unit is-set-LEM

-- Strengthened to an untruncated sum
requirement1 : (F G : Aut X) → (F ＝ id-equiv) + (G ＝ id-equiv) + (F ＝ G)
requirement1 F G with map-equiv F (inl star) in F-inl-eq | map-equiv G (inl star) in G-inl-eq
... | inl star | _ = inl (inl-action-id F F-inl-eq)
... | inr lem | inl star = inr (inl (inl-action-id G G-inl-eq))
... | inr lem | inr lem' rewrite LEM-ext lem' lem = inr (inr ((inl-action-swap F lem F-inl-eq) ∙ inv (inl-action-swap G lem G-inl-eq)))

requirement2 : (Aut X ≃ unit + unit) → LEM l
requirement2 eq = cases where

  F : Aut X
  F = map-inv-equiv eq (inl star)

  G : Aut X
  G = map-inv-equiv eq (inr star)

  cases : LEM l
  cases with map-equiv F (inl star) in F-inl-eq | map-equiv G (inl star) in G-inl-eq
  ... | inl star | inr lem' = lem'
  ... | inr lem | _ = lem
  ... | inl star | inl star with is-injective-equiv (inv-equiv eq) (inl-action-id F F-inl-eq ∙ inv (inl-action-id G G-inl-eq))
  ... | ()

requirement3 : (Aut X ≃ unit) → ¬ LEM l
requirement3 eq lem with absurd where

  id-is-swap : id-equiv ＝ swap lem
  id-is-swap = is-injective-equiv eq refl

  absurd : inl star ＝ inr lem
  absurd = ap (λ H → map-equiv H (inl star)) id-is-swap

... | ()

requirement2+3 : (Aut X ≃ unit + unit) ↔ LEM l
requirement2+3 .pr1 = requirement2
requirement2+3 .pr2 lem = pair identify-aut identify-aut-is-equiv where

  identify-aut : Aut X → unit + unit
  identify-aut F with map-equiv F (inl star)
  ... | inl star = inl star
  ... | inr lem' = inr star
    
  reconstruct-aut : unit + unit → Aut X
  reconstruct-aut (inl star) = id-equiv
  reconstruct-aut (inr star) = swap lem

  identify-aut-section : (t : unit + unit) → identify-aut (reconstruct-aut t) ＝ t
  identify-aut-section (inl star) = refl
  identify-aut-section (inr star) = refl

  identify-aut-retraction : (F : Aut X) → reconstruct-aut (identify-aut F) ＝ F
  identify-aut-retraction F with map-equiv F (inl star) in F-inl-eq
  ... | inl star = inv (inl-action-id F F-inl-eq)
  ... | inr lem' rewrite LEM-ext lem' lem = inv (inl-action-swap F lem F-inl-eq)

  identify-aut-is-equiv : is-equiv identify-aut
  identify-aut-is-equiv = is-equiv-is-invertible reconstruct-aut identify-aut-section identify-aut-retraction

requirement2' : (F : Aut X) → F ≠ id-equiv → LEM l
requirement2' F H with map-equiv F (inl star) in F-inl-eq
... | inl star = ex-falso (H (inl-action-id F F-inl-eq))
... | inr lem = lem