```{-
Auke Booij, February 2016

In Univalent Foundations, if there is a polymorphic function f_X : X → X, such
that f₂ is not the identity function, then LEM holds.

http://www.cs.bham.ac.uk/~abb538/papers/2016-02-parametricity.pdf

and the blog post at

http://homotopytypetheory.org/2016/02/24/parametricity-and-excluded-middle/
-}

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

module nonparametric where

open import HoTT

transport-fst : ∀ {i j k} {A : Type i} (B : A → Type j) (C : (z : A) → B z → Type k) {x y : A} (p : x == y) (u : B x) (v : C x u) → fst (transport (λ z → Σ (B z) (C z)) p (u , v)) == transport B p u
transport-fst B C idp u v = idp
transport-snd' : ∀ {i j k} {A : Type i} (B : A → Type j) (C : A → Type k) {x y : A} (p : x == y) (u : B x) (v : C x) → snd (transport (λ z → B z × C z) p (u , v)) == transport C p v
transport-snd' B C idp u v = idp

polymorphicFun : Type (lsucc lzero)
polymorphicFun = {X : Type lzero} → X → X

flip : Bool → Bool
flip true = false
flip false = true

flip-eq : Bool ≃ Bool
flip-eq = equiv flip flip flip-id flip-id
where
flip-id : (b : Bool) → flip (flip b) == b
flip-id true = idp
flip-id false = idp

false-true-fun : Type (lsucc lzero)
false-true-fun = Σ polymorphicFun (λ f → f {Bool} false ≠ false)

true-false-fun : Type (lsucc lzero)
true-false-fun = Σ polymorphicFun (λ f → f {Bool} true ≠ true)

is-non-id : {X : Type lzero} → polymorphicFun × X → Type lzero
is-non-id {X} (f , b) = f {X} b ≠ b

non-id-fun : (X : Type lzero) → Type (lsucc lzero)
non-id-fun X = Σ (Σ polymorphicFun (λ _ → X)) is-non-id

prop : ∀ {i} → Type (lsucc i)
prop {i} = Σ (Type i) is-prop

decidable : ∀ {i} → Type i → Type i
decidable X = X ⊔ ¬ X

LEM : ∀ {i} → Type (lsucc i)
LEM {i} = (P : prop {i}) → decidable (fst P)

efq : ∀ {i} {X : Type i} → ⊥ → X
efq = ⊥-rec

Three : ∀ {i} → (P : prop {i}) → Type i
Three P = Suspension (fst P) ⊔ Unit

-- re-defining this to get computational equality in the first argument
inhab-prop-is-contr' : ∀ {i} {A : Type i} → A → is-prop A → is-contr A
inhab-prop-is-contr' x₀ p = (x₀ , λ y → fst (p x₀ y))

inhab-susp : {P : prop {lzero}} → fst P → is-contr (Suspension (fst P))
inhab-susp {P} p = north (fst P) , Suspension-elim (fst P) idp (merid (fst P) p) q
where
q' : (x : Suspension (fst P)) (q : north (fst P) == x) → PathOver (λ z → north (fst P) == z) (merid (fst P) p) idp (merid (fst P) p)
q' x q = J (λ a' p → PathOver (λ z → north (fst P) == z) p idp p) idp (merid (fst P) p)
q : (x : fst P) → PathOver (λ z → north (fst P) == z) (merid (fst P) x) idp (merid (fst P) p)
q x =
transport
(λ y → PathOver (λ z → north (fst P) == z) (merid (fst P) y) idp (merid (fst P) p))
(snd (inhab-prop-is-contr' p (snd P)) x)
(q' (north (fst P)) idp)

swap : ∀ {i} {X : Type i} → Suspension X → Suspension X
swap = flip-susp

extract : {P : prop {lzero}} (q : north (fst P) == south (fst P)) → fst P
extract {P} q = transport code q tt
where
code : Suspension (fst P) → Type lzero
code x = SuspensionRecType.f (fst P) {j = lzero} Unit (fst P) (λ p → contr-equiv-Unit (inhab-prop-is-contr p (snd P)) ⁻¹) x

↓-contr : ∀ {i j} {A : Type i} {B : A → Type j} {x y : A} {p : x == y} (u : B x) (v : B y)
(h : (a : A) → is-contr (B a))
→ u == v [ B ↓ p ]
↓-contr {_} {_} {_} {_} {x} {_} {idp} u v h = ! (snd (h x) u) ∙ (snd (h x) v)

extract' : {P : prop {lzero}} (x : Suspension (fst P)) (q : x == swap x) → fst P
extract' {P} x q =
SuspensionElim.f
(fst P)
{P = λ x → x == swap x → fst P}
(extract {P = P})
((extract {P = P}) ∘ ap swap)
(λ p → ↓-contr extract (extract ∘ ap swap) (λ _ → WeakFunext.weak-λ= (λ _ → inhab-prop-is-contr p (snd P))))
x
q

inhabited-equiv-susp : {P : prop {lzero}} → fst P → Bool ≃ (Three P ≃ Three P)
inhabited-equiv-susp {P} p = equiv f g f-g g-f
where
paths : (a b : Suspension (fst P)) → inl a == (inl b :> Three P)
paths a b = ap inl (contr-has-all-paths (inhab-susp {P = P} p) a b)
three-eq : Three P ≃ Three P
three-eq = equiv f3 f3 g-f3 g-f3
where
f3 : Three P → Three P
f3 (inr tt) = inl (north (fst P))
f3 (inl x) = inr tt
g-f3 : (o : Three P) → f3 (f3 o) == o
g-f3 (inr tt) = idp
g-f3 (inl x) = paths (north (fst P)) x
f : Bool → (Three P ≃ Three P)
f false = ide (Three P)
f true = three-eq
g : (Three P ≃ Three P) → Bool
g e with –> e (inr tt)
... | inr tt = false
... | inl _  = true
g-f : (b : Bool) → g (f b) == b
g-f false = idp
g-f true = idp
deduce-idf : (e : Three P ≃ Three P) (q : –> e (inr tt) == inr tt) → e == ide (Three P)
deduce-idf e q = subtype=-in is-equiv-is-prop (cases (–> e (inl (north (fst P)))) idp)
where
cases : (pt : Three P) (q' : –> e (inl (north (fst P))) == pt) → –> e == idf (Three P)
cases (inr tt) q' =
efq (inl≠inr (north (fst P)) tt (
! (is-equiv.g-f (snd e) (inl (north (fst P))))
∙ ap (is-equiv.g (snd e)) (q' ∙ ! q)
∙ is-equiv.g-f (snd e) (inr tt)
))
cases (inl y)  q' = FunextNonDep.λ=-nondep pted
where
pted : (pt' : Three P) → –> e pt' == pt'
pted (inr tt) = q
pted (inl z)  = ap (–> e) (paths z (north (fst P))) ∙ q' ∙ paths y z
deduce-three : (e : Three P ≃ Three P) {u : Suspension (fst P)} (q : –> e (inr tt) == inl u) → e == three-eq
deduce-three e {u} q = subtype=-in is-equiv-is-prop (cases (–> e (inl u)) idp)
where
cases : (pt : Three P) (q' : –> e (inl u) == pt) → –> e == –> three-eq
cases (inl y)  q' = efq (inl≠inr u tt (
! (is-equiv.g-f (snd e) (inl u))
∙ ap (is-equiv.g (snd e)) (q' ∙ paths y u ∙ ! q)
∙ is-equiv.g-f (snd e) (inr tt)
))
cases (inr tt) q' = FunextNonDep.λ=-nondep pted
where
pted : (pt' : Three P) → –> e pt' == –> three-eq pt'
pted (inr tt) = q ∙ paths u (north (fst P))
pted (inl z)  = ap (–> e) (paths z u) ∙ q' ∙ ap (–> three-eq) (paths (north (fst P)) z)
f-g : (e : Three P ≃ Three P) → f (g e) == e
f-g e = cases (–> e (inr tt)) idp
where
cases : (pt : Three P) (q : –> e (inr tt) == pt) → f (g e) == e
cases (inr tt) q = transport (λ d → f (g d) == d) (! (deduce-idf e q)) idp
cases (inl y) q = transport (λ d → f (g d) == d) (! (deduce-three e q)) idp

inhabited-equiv-idf : {P : prop {lzero}} → fst P → (e : Three P ≃ Three P) → (–> e (inr tt) == inr tt) → –> e == idf (Three P)
inhabited-equiv-idf {P} p e q = FunextNonDep.λ=-nondep pted
where
paths : (a b : Suspension (fst P)) → inl a == (inl b :> Three P)
paths a b = ap inl (contr-has-all-paths (inhab-susp {P = P} p) a b)
pted : (x : Three P) → –> e x == x
pted (inl p') = ind (–> e (inl p')) idp
where
ind : (y : Three P) → (q' : –> e (inl p') == y) → –> e (inl p') == inl p'
ind (inl p'') q' = q' ∙ paths p'' p'
ind (inr tt)  q' =
q'
∙ ! (is-equiv.g-f (snd e) (inr tt))
∙ ap (is-equiv.g (snd e)) (q ∙ ! q')
∙ is-equiv.g-f (snd e) (inl p')
pted (inr tt) = q

false-true-LEM : (F : false-true-fun) → LEM {lzero}
false-true-LEM (f , f-neq) P = cases1 (g (inr tt)) idp
where
g-eq : Three P ≃ Three P
g-eq = f {Three P ≃ Three P} (ide (Three P))
g : Three P → Three P
g = –> g-eq
module _ (p : fst P) where
three-eq : Bool ≃ (Three P ≃ Three P)
three-eq = inhabited-equiv-susp {P = P} p
g-neq : Σ (Three P ≃ Three P) (λ pt → f {Three P ≃ Three P} pt ≠ pt)
g-neq = transport (λ X → Σ X (λ x → f {X} x ≠ x)) (ua three-eq) (false , f-neq)
g-eq-neq : g-eq ≠ ide (Three P)
g-eq-neq = transport (λ x → f x ≠ x) path (snd g-neq)
where
path : fst g-neq == ide (Three P)
path =
transport-fst
(λ X → X)
(λ X x → f {X} x ≠ x)
(ua three-eq)
false
f-neq
∙ ap
(λ x → coe x false)
(ap-idf (ua three-eq))
∙ coe-β three-eq false
cases1 : (x : Three P) (q : g (inr tt) == x) → decidable (fst P)
cases1 (inr tt) q = inr proof
where
p1 : (p : fst P) → g == idf (Three P)
p1 p = inhabited-equiv-idf {P = P} p g-eq q
proof : (p : fst P) → ⊥
proof p = g-eq-neq p (subtype=-in is-equiv-is-prop (p1 p))
cases1 (inl x)  q = cases2 (g (inl x)) idp
where
cases2 : (y : Three P) (r : g (inl x) == y) → decidable (fst P)
cases2 (inl y)  r = inr proof
where
proof : (p : fst P) → ⊥
proof p = inl≠inr x tt (
! (is-equiv.g-f (snd g-eq) (inl x))
∙ ap (is-equiv.g (snd g-eq)) (r ∙ ap inl (contr-has-all-paths (inhab-susp {P = P} p) y x) ∙ ! q)
∙ is-equiv.g-f (snd g-eq) (inr tt)
)
cases2 (inr tt) r = cases3 (g (inl (swap x))) idp
where
cases3 : (z : Three P) (s : g (inl (swap x)) == z) → decidable (fst P)
cases3 (inl z)  s = inr (λ p → inr≠inl tt z (
! r
∙ ap (g ∘ inl) (contr-has-all-paths (inhab-susp {P = P} p) x (swap x))
∙ s)
)
cases3 (inr tt) s = inl (extract' {P = P} x (–> (inl=inl-equiv x (swap x)) (
! (is-equiv.g-f (snd g-eq) (inl x))
∙ ap (is-equiv.g (snd g-eq)) (r ∙ ! s)
∙ is-equiv.g-f (snd g-eq) (inl (swap x))
)))

true-false-LEM : (F : true-false-fun) → LEM {lzero}
true-false-LEM (f , f-neq) = false-true-LEM (f' , f-neq')
where
f-as : non-id-fun Bool
f-as = ((f , true) , f-neq)
f-as' : non-id-fun Bool
f-as' = transport non-id-fun (ua flip-eq) f-as
f' : polymorphicFun
f' = fst (fst f-as')
f-neq' : f' {Bool} false ≠ false
f-neq' = transport
(λ b → f' b ≠ b)
(
ap snd (
transport-fst
(λ X → Σ polymorphicFun (λ _ → X))
(λ X b → is-non-id {X} b)
(ua flip-eq)
(fst f-as)
f-neq
)
∙ transport-snd' (λ _ → polymorphicFun) (idf Set) (ua flip-eq) f true
∙ ap (λ x → coe x true) (ap-idf (ua flip-eq))
∙ coe-β flip-eq true
)
(snd f-as')

non-id-LEM : (f : polymorphicFun) → (f {Bool} ≠ idf Bool) → LEM {lzero}
non-id-LEM f neq = cases1 (f false) idp
where
cases1 : (b : Bool) (p : f false == b) → LEM {lzero}
cases1 true  p = false-true-LEM (f , λ q → Bool-false≠true (! q ∙ p))
cases1 false p = cases2 (f true) idp
where
cases2 : (b : Bool) (p : f true == b) → LEM {lzero}
cases2 true q  = efq (neq (FunextDep.λ= f-id))
where
f-id : (b : Bool) → f b == b
f-id true = q
f-id false = p
cases2 false q = true-false-LEM (f , (λ r → Bool-true≠false (! r ∙ q)))
```